- Compiler Technology Department
- Computer Systems Department
- Information Systems Department
- Software Engineering Department
- System integration and multi-disciplinary collaborative environments
- System Programming Department
- Theoretical Computer Science Department
- Academic council
- Dissertation council
- Verification Center of the Operating System Linux
- Center of competence in parallel and distributed computing
Equivalence checking of sequential programs with the help of two-tape automata.
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).
program, equivalence, multi-tape automaton