Computer Science, № 28, 2008

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.

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

Nets of active resources (AR-nets) are presented. This formalism has the same expressive power as Petri nets but a different syntax: the model is not a bipartite oriented graph, but an oriented graph with two types of arcs (consumption and production). Direction of the arc denotes active and passive participants...

Formal models for real-time systems have been actively studied over the past several years. Much of the theory of untimed systems has been lifted to the real-time setting. An example is the notion of trace equivalence applied to timed transition systems with invariants which is studied here within the general...

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

Structures of data and ontology arising in information systems containing facto-graphical data are considered.

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

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

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