Program equivalence checking by two-tape automata.

Authors

Zakharov V.A.

Abstract

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

Keywords

program, equivalence, multi-tape automaton

Edition

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

Research Group

Theoretical Computer Science

All publications during 2011

All publications