Preprints of IIS SB RAS, 2006

This paper presents C#-light, an input language of the C#-program verification system, and C#-kernel, an internal language that is used in the three-level scheme of verification. The algorithms for translation from C#-light into C#-kernel are considered.

This paper describes an application of the new three-level approach to verification of programs in C#-light, which is a significant sequential C# subset. At the first stage, C#-light is translated into an intermediate language C#-kernel. At the second stage, lazy verification conditions are generated by means of axiomatic semantics of C#-kernel. The verification conditions are lazy because they can include symbols representing postponed extractions of label invariants as well as postponed invocations of methods and delegates. At the third stage, lazy verification conditions are refined using some algorithms of operational semantics. The paper's goal is to apply our approach to verification of some programs (originally written in Java) which proved to be verification challenges in the system ESC/Java. In addition, the issue of verification condition simplification is considered.

Project F@BOOL@ is aimed to development of a transparent, compact, and portable verifying compiler. It is assumed that F@BOOL@ will exploit efficient decision procedures for validation of correctness conditions (instead of semiautomatic theorem provers). In particular, F@BOOL@ will extensively use SAT-solvers for validation of Boolean encoding of correctness conditions. The target group of F@BOOL@ users comprises Computer Science, Information Technology and Mathematics students willing to comprehend program verification.

The technical report is the second part of F@BOOL@ documentation. It presents informal introduction to Floyd-style verification of program, formal syntax, static and run-time semantics of Logical Annotations for a toy programming language Mini-NIL. (This language is a prototype of F@BOOL@ virtual machine.)

The intention of the work is to develop structural algorithms to eRectively analyze the behavioural properties (e.g., liveness, divergency, boundedness, safety) of diRerent subclasses of dense-time Petri nets. The algorithms are implemented within the RT-MEC system (Real Time Model and Equivalence Checker) supporting specification, analysis, validation and verification of distributed and real-time systems represented by various timed PN-based models.

Logo is a recognized programming language for elementary teaching of programming to children. This preprint describes how this language can be used for solving the tasks specially designed to encourage the thinking and cognitive ability of younger pupils. These tasks will help them to learn the basis of programming in a fascinating and accessible form and to stimulate their interest to computer science.

In this paper we consider formal representation of knowledge as an (elementary) first-order logical theory. We study the decomposability property of theories, which means the possibility to split a formal representation of a considered subject domain into parts, each described by a separate set of terms. The decomposability problem is reduced to the question of minimization of system of axioms for a theory. We formulate the criterion of decomposability and prove the uniqueness of signature decomposition, as well as the uniqueness of theory decomposition up to equality formulas.

In this paper we consider declarative knowledge bases as first-order (elementary) theories. We study an operation of incremental data extraction, which is closely connected with query reformulation in information retrieval and data integration. We introduce a formal definition of this operation and provide it with semantics in terms of lattices by using the main theorem of Formal Concept Analysis.

The intention of the paper is to achieve an hierarchy of interconnections for a number of trace equivalences and bisimulations on a context of hybrid-time event structures and prime event structures.