A three-stage method of C program verification

A three-stage method of C program verification is presented. It is a further development of the two-stage method in the framework of the C-light project. An additional stage of normalization of C-light programs is introduced and optimization of the two-stage method caused by this introduction is considered.

anureev.pdf604.02 KB

On the problem of computer language classification

During the semicentenial history of Computer Science and Information Technologies, several thousands of computer languages have been created. Computer language universe includes languages for different purposes: programming languages, specification languages, modeling languages, languages for knowledge representation, etc. In each of these branches of computer languages it is possible to track...

anureev_bodin.pdf116.79 KB

Some algorithms of image processing and their reflection onto multiprocessor systems

Problems related to reflection of some algorithms of image processing onto multiprocessor systems are investigated. In particular, algorithms of allocation of contours, such as the gradient method and the combinatorial method (the method of the threshold gradient), are considered. In view of complexity of the algorithm of searching objects on...

kalinnikov.pdf288.67 KB

Parallel implementation of the Ramalingam decremental algorithm for dynamic updating the single-sink shortest paths subgraph

We propose an efficient parallel implementation of the Ramalingam algorithm for dynamic updating the single-sink shortest paths subgraph of a directed weighted graph after deletion of an edge on a model of associative (content addressable) parallel systems with vertical processing (the STAR-machine). The associative version of the Ramalingam decremental algorithm...

nepomniaschaya_a_sh.pdf169.4 KB

On decomposability in logical calculi

In the paper, a natural class of logical calculi is fixed for which we formulate the notion of a Δ -decomposable set of formulas. We demonstrate that the property of uniqueness of signature decompositions holds in those calculi of this class that have the Craig interpolation property. In conclusion, we...

ponomaryov.pdf143.58 KB

A notion of congruence for dtsPBC

Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched with iteration. In this paper, we define a number of stochastic equivalences for dtsPBC which allow one to identify finite and infinite stochastic processes with similar behaviour. A problem of preservation of the...

tarasyuk.pdf242.97 KB