Ivannikov Institute for System Programming of the RAS

Program equivalence checking by two-tape automata.


Zakharov V.A.


This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If a dynamic frame is acyclic (i.e., all program statements are irreversible), it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs operating on the dynamic frame can be reduced to the emptiness problem for two-tape automata (compound machine).

Text of article


program, equivalence, multi-tape automaton


Cybernetics and Systems Analysis, 2011, vol 46, № 4, pp. 554-562.

Research Group

Theoretical Computer Science

All publications during 2011 All publications