2021/09/04 by Manish Goyal, Muqsit Azeem, Goyal, Manish +5
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Software Engineering (cs.SE) #Software Engineering Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2109.01864
openalex publication_date 2021/09/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.