Partial SSA form: compact representation for programs with indirect memory operations
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...
Ontology-based approach to development of adjustable knowledge internet portal for support of research activitiy
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...
OS-independent detection of thread switches on uniprocessor
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...
Efficient update of tree paths on associative systems with bit-parallel processing
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)...
Symbolic verification method for definite iterations over tuples of altered data structures
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...
Constraint-based analysis of composite solvers
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...
Designing tableau-like axiomatization for Propositional Linear Temporal Logic at home of Arthur Prior
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.