Preprints of IIS SB RAS, 2001

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.

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.

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.

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.

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.