Direct Construction of Program Alignment Automata for Equivalence Checking

TL;DR

This paper introduces a direct algorithm for constructing program alignment automata to check program equivalence, overcoming limitations of trace-based methods by avoiding incomplete behavior coverage.

Contribution

It proposes a novel direct construction method for program alignment automata, improving accuracy and completeness over trace-based approaches.

Findings

The direct construction method effectively handles program dissimilarities.

It reduces issues related to incomplete behavior coverage.

The approach enhances the reliability of equivalence checking.

Abstract

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.