Automata-theoretic approach to the equivalence checking problem for sequential programs

VCLA hosted a talk by Vladimir Zakharov on June 1st, 2012.

ABSTRACT

The automata-theoretic approach has been widely used in software verification since the very beginning of computer science. The aim of this talk is to show how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. At a certain level of abstraction the semantics of sequential programs can be defined in terms of dynamic logic structures. In some cases these structures can be specified by means of two-tape automata. Then the equivalence checking for a pair of sequential programs operating on the dynamic frame can be reduced to the emptiness problem for a two-tape automaton which describes all pairs of compatible computations of these programs. We consider the cases when the emptiness of such an automaton can be checked effectively in polynomial time. The obtained results show that to build an efficient equivalence checking algorithm for sequential programs all one needs is to find a suitable two-tape automaton which specifies the semantics of the programs. This reduction technique opens a new way for the application of multi-tape automata to program analysis and verification.