Preprints of IIS SB RAS, 2006

Preprint 141
Vladimir A. Evstigneev, Ruslanbek N. Arapbaev, Rafhat A. Osmonov
Comparative analysis of tests for data dependence

In the paper, we present a comparative review of tests for data dependence that are applied in parallelizing compilers. Comparisons of power and limits of tests characteristics of different criteria are given both on examples and under estimated.

Key words: parallelizing compilers, data dependence, loop parallelization, optimization, linear Diophantine equation.

Preprint 140
I.V. Dubranovsky
Towards C#-program verification: algorithms of translation from C#-light into C#-kernel

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.

Preprint 139
A.V. Promsky
Application of three-level approach to C#-light program verification
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.

Preprint 138
E. Bodin, N. Kalinina, N. Shilov
Verifying compiler F@BOOL@ Part II: Logical annotations in Mini-NIL, their static and run-time semantics

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.)

Preprint 137
A.V. Bystrov
Structural analysis of dense-time Petri nets behaviour

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.

Preprint 136
N.S. Vodopyanova, N.V. Sosedkina, T.I. Tikhonova, A.V. Lystsov
Logo programming for elementary school

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.

Preprint 135
Denis Ponomaryov
Formal Knowledge Representation and the Decomposability Problem

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.

Preprint 134
Denis Ponomaryov
Lattice Semantics for Incremental Data Extraction from Declarative Knowledge Bases
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.

Preprint 133
N.S. Usotskaya
Investigation of equivalences on a context of hybrid-time event structures

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.

Preprint 132
Alexander Stasenko, Alexey Sinyakov
Basic means of the Sisal 3.1 language

ВThis work describes syntax and semantics of the new version of dataflow programming language Sisal 3.1, being the source language of the system of functional programming (SFP) developed as a part of the project PROGRESS. Language Sisal 3.1 is obtained by simplification, improvement, expansion and specification of the Sisal 90 language user manual. It also uses some ideas of Sisal 3.0 language and elements of the object-oriented approach. New user types, operations redefinition and overloading of functions are elements of the objectoriented approach in Sisal 3.1 language.

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.