Two-tape machinery for the equivalence checking of sequential programs.
Two-tape machinery for the equivalence checking of sequential programs.
Authors
Abstract
This paper presents a new automata-theoretic approach to equivalence checking of sequential programs whose semantics is described by means of dynamic logic structures. A distinguished feature of this approach is an active utilization of two-tape automata in decision procedures. Our approach provides a uniform framework for designing effective algorithms (including polynomial time ones) by reducing the equivalence checking problem for sequential programs $\pi_1$ and $\pi_2$ operating on a dynamic frame $\Fc$ to the analysis of two-tape automata which describes all pairs of compatible computations of $\pi_1$ and $\pi_2$. As a result, to build an efficient equivalence checking algorithm all one needs is to find a suitable two-tape automaton which specifies the equivalence relation induced by a dynamic frame $\Fc$ on the set of finite sequences of basic actions (program statements). This forges the way for the application of multi-tape automata to program analysis and verification.
Edition
Proceedings of the International Workshop on Program Understanding, June 20-22, 2009, Novosibirsk, 2009, Novosibirsk, pp. 28-40.
Research Group
All publications during 2009
All publications