Computer Science, № 15, 2001

A new specification language, simple to master, is suggested. In spite of simplicity, this language is expressive enough. A decision method for its quantifier-free formulas is given. A program verification method based on this language is illustrated by an example of a program of bubble sorting.

In the paper, we construct a formula that characterizes a timed event structure up to the timed must-preorder.

This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which want to participate in a step...

A lot of work has been dedicated to the analysis of sequential imperative programs. However, existing tools of analysis seem to lack for clarity and extensibility. That is to say, although some of them perform powerful context-sensitive dataflow analysis, their efforts are chiefly directed to the analysis of a particular...

In this paper, the model-checking algorithm from [22] is adapted to coloured Petri nets (CPN) [9, 10]. The state-based semantics of LTL for CPN is given and the correctness of the obtained approach is proven. It is also shown how to apply this model checking technique to interval-timed CPN.

The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow tuples of data structures and exit from the iteration body under a condition. Transformations of these generalized iterations to the standard ones are proposed and justified. Useful properties of the transformations are given. A technique...

There are lots of different approaches developed for global static program error analysis. Most of them are concentrated on sequential programs. Analysis of parallel programs is considered complicated. The overview contains brief information on obsolete and modern approaches to global static error analysis of parallel programs.

R.N. Taylor has proposed Call...

A formal model of the state of a dynamic system with updateable locations as values is presented. A mechanism of dynamic function declaration resembling that of variable declaration in programming languages is suggested.With each of these functions a dynamic access function is associated. An access function can be used either...