Program verification based on the specification language SIMPLE
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.
Towards decidability of timed testing
In the paper, we construct a formula that characterizes a timed event structure up to the timed must-preorder.
Net and algebraic approaches to probabilistic modeling
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...
An extensible analyzer of subroutines in imperative languages
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...
LTL model checking of coloured Petri nets based on net unfoldings
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.
Symbolic verification method for definite iterations over tuples of data structures
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...
Overview of approaches to global static error analysis of parallel programs
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...
Typed ASMs with updateable locations as values
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...