The paper presents an improvement over traditional SSA form, called partial SSA that features only partial translation of a program into the singleassignment state. Partial SSA is more compact than the traditionally used full SSA while it suits well most program optimization algorithms. The paper…
This paper presents an approach to the development of specialized Internet portals providing content-based access to systematized knowledge and information resources, relating to a certain branch of science. The information basis of such portals is formed by ontologies, containing the description of…
Parallel programs often are non-deterministic in their nature, what greatly complicates testing, debugging, verifying and analyzing such programs. On a uniprocessor, interleaving actions of the system scheduler (thread switches) can be thought of as source of nondeterminism. The precise detection of…
In this paper, we propose an efficient associative parallel algorithm for updating tree paths after every change in the underlying graph. Such a problem arises when we perform dynamic graph algorithms. To speed up time complexity of the algorithm, we use a new associative model called associative…
In order to extend the area of application of the symbolic verification method [19, 20, 21, 22, 23], definite iterations over tuples of altered data structures are introduced and reduced to the standard definite iterations. This reduction is extended to definite iterations including the exit…
Cooperative constraint solving is an area of constraint programming that studies the interaction between constraint solvers with the aim of discovering the interaction patterns that amplify the positive qualities of individual solvers. Automatisation and formalisation of such studies is an important…
Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. The paper suggests a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the…