Preprints of IIS SB RAS, 2001

Preprint 89
Kozura V.E., Nepomniaschy V.A., Novikov R.M.
Verification coloured petri nets by model checking method

A verification tool PNV (Petri net verifier) based on model checking method has been developed and implemented. The tool PNV is applied to coloured Petri nets limited by finite state systems when properties are presented in mu-calculus. The paper describes PNV and verification experiments with coloured Petri nets which model alternating bit and ring communication protocols as well as dining philosophers.

Preprint 88
M. F. Murzina
On prolongation of geodesics in the cayley graphs of some groups

The Cayley graph - one of classicalmodels for representation of algebraic groups. In the preprint the problem of prolongation of the shortest paths (geodesic) in the graphs of some hyperbolic groups and groups of integers on addition is studied. The performance of deadlock tops (that is, from which there is no exit on an edge with magnification of length) in the considered Cayley graphs is given.

Preprint 87
V. A. Nepomniaschy, I. S. Anureev, I.N. Michailov, A. V. Promsky
Towards the verification of c programs. part 2. language c-light-kernel and its axiomatic semantics

A language C-light-kernel suitable for verification is described. This language is a kernel of the C-light language. Axiomatic semantics of C-lightkernel is defined and its soundness with respect to operational semantics is proved. We suggest to use C-light as an input language for a program verification tool which includes a translator to C-light-kernel and a verification condition generator for C-light-kernel programs.

Preprint 86
Dmitry F. Semich
Development of the mathematical model and realization of lowbitrate high-perfomance digital videocompression technology

This article describes the mathematical model and realization example of lowbitrate high-performance videocodec. Positive difference of this model from other similar models is quality of compressed video. This model can produce quality of MPEG-2 3.5Mbit videostream within 1 Mbit bitrate.

Preprint 85
A. A. Yakovlev
Free osES. analysis of current situation

This work represents an overview of general situation in current attitude among free software. It emphasizes mostly on the operational systems and particularly on products provided by Free Software Foundation (FSF) directed by Richard Stollman. Operational systems and software analyzed are UNIX-based and UNIX-like. The goal was to create objective point of view on the perspective of free software development competing with similar copy-righted commercial products. To realize this few examples of tests were presented. Tests were based on not too much detailed overview of such OSes like Linux Red Hat 5.0/5.2, Free BSD 2.2.6/3.0, Solaris 7, UnixWare 7. Features investigated are process of installation, user interface, language support, security issues, software available for analyzed OS (such as Web-server Apache, GCC etc.) and remarks about documentation. Growth of free software popularity is presented by statistics gathered from various Internet recourses and independent groups. As reference for the investigated topic a short list of helpful literature is presented at the end of work. Appendix contains list of GNU and other utilities available with distributions of free software.

Preprint 84
V. A. Nepomniaschy, I. S. Anureev, I.N. Michailov, A. V. Promsky
Towards c programs verification. part 1. language c-light

A language C-light which is a representative subset of the language C is proposed. This language includes deterministic expressions, statements switch and goto with some restrictions as well as the functions new and delete for processing the dynamic memory. It imposes some restrictions on the use of types of the language C. Complete structural operational semantics in Plotkin style is presented for C-light. Using C-light as an input language of a program verification system is suggested.

Preprint 81
Serge I. Katkov
The system of parallel programming superpascal: language, translator, debugger

The parallel programming system is based on the programming language SuperPascal. Using this system, a parallel algorithm can be debugged on PC. The system can be used for teaching parallel programming or creation and debugging of parallel algorithms.




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.