Direct Construction of Program Alignment Automata for Equivalence Checking
This work addresses a fundamental challenge in program verification for developers and researchers, offering a more reliable method for equivalence checking, though it appears incremental as it builds on existing alignment predicate techniques.
The paper tackles the problem of checking semantic equivalence between two programs by introducing a direct algorithm to construct program alignment automata, avoiding the need for trace-based methods that can lead to incomplete results.
The problem of checking whether two programs are semantically equivalent or not has a diverse range of applications, and is consequently of substantial importance. There are several techniques that address this problem, chiefly by constructing a product program that makes it easier to derive useful invariants. A novel addition to these is a technique that uses alignment predicates to align traces of the two programs, in order to construct a program alignment automaton. Being guided by predicates is not just beneficial in dealing with syntactic dissimilarities, but also in staying relevant to the property. However, there are also drawbacks of a trace-based technique. Obtaining traces that cover all program behaviors is difficult, and any under-approximation may lead to an incomplete product program. Moreover, an indirect construction of this kind is unaware of the missing behaviors, and has no control over the aforesaid incompleteness. This paper, addressing these concerns, presents an algorithm to construct the program alignment automaton directly instead of relying on traces.