Equivalence checking of sequential programs with the help of two-tape automata.

Authors

V.A. Zakharov

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).

Keywords

program, equivalence, multi-tape automaton

Research Group

Theoretical Computer Science

All publications during 2010

All publications