Computer Science, № 23, 2005

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 introduces formal quality criteria for...

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 scientific and research activity as a whole as...

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 these actions helps many tasks, especially the schedule-based execution...

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 graph machine (AG-machine)...

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 statement. The generalization of the...

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 issue of cooperative constraint solving.

In this paper, we...

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 propositional μ-Calculus.