Preprints of IIS SB RAS, 1998

Preprint 56
T.G. Churina
Coloured Petri nets approach to the validation of SDL-specifications

This work is devoted to research dealing with automated constructing net models of SDL specifications. In the paper is considered SDL specifications with timers and priorities. The specifications allows to represent a considerable class of communication protocols. Coloured Petri nets extended by priorities and Merlin's time concepts are used as the net models. This work describes a method of translating the SDL specification into the net models.

Preprint 55
I.S. Anureev
Formula rewriting systems application to automated program verification

The methodology of applying formula rewriting systems to automated program verification is suggested. The possibility of automated verification of a number of programs of text editing, array sorting and file sorting is demonstrated. The verification system SPECTRUM module combining simplification procedures based on formula rewriting systems with other decision and simplification procedures is described.

Preprint 54
I.S. Anureev
Formula rewriting system theory

Formula rewriting system theory is represented. The unified approach to correctness definition of such systems is suggested. A relation between formula rewriting systems and type theories is considered. A survey of classes of terminating formula rewriting systems is given.

Preprint 51
Michael A. Bulyonkov, Dmitry V. Kochetov
Visualization of program properties

This paper presents a model of program properties. This model does not depend on programming languages and application areas. Also properties visualizer HyperCode is described in the paper. This tool is implemented for integration into different programming and software reengineering systems.

Preprint 50
A.E. Ryazanov
System BUTSEPHALAS: defining proof-search strategies and combining deductive procedures

We present a semiautomatic theorem prover based on the notion of strategy. Main emphasis is made on description of the strategy definition language which is the key point in design of the system. Declarative and informal operational semantics of the language are described. Substantial number of examples illustrating features of the language is devoted to combining heterogeneous deductive procedures into a single proof-search strategy.

Preprint 49
D.M. Ushakov
Some formal aspects of subdefinite models

General methods for problem solving are objects of study in artificial intelligence. This work describes subdefinite models as a framework for solving constraint satisfaction problems. Such problems arise in many fields of science and engineering. The use of the method of constraint propagation in subdefinite models makes it possible to estimate the set of all solutions of such a problem. Foundations of subdefinite models are given in the paper. The notion of subdefinite extension of a many-sorted model is proposed, and the types of such extensions are discussed. Both denotational and operational semantics of constraint propagation in subdefined models are defined and their equivalence is proved.

Preprint 48
S.K. Chernonozhkin
Program profiling facilities in the SOKRAT project

The system of profiling assembler and Modula-2 programs which has been implemented in the frameworks of the SOKRAT project, is described. Necessary definitions are given and possible approaches to implementation of these systems are analyzed. Main characteristics of the approach used in the project are considered. Examples of the work of the system are given.




You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.