Nuno P. Lopes and José Monteiro
Proving the equivalence of programs has several important applications, including algorithm recognition, regression checking, compiler optimization verification, and information flow checking.
Despite being a topic with so many important applications, program equivalence checking has seen little advances over the past decades due to its inherent (high) complexity.
In this paper, we propose, to the best of our knowledge, the first algorithm for the automatic verification of partial equivalence of two programs over the combined theory of uninterpreted function symbols and integer arithmetic (UF+IA). The proposed algorithm supports, in particular, programs with nested loops.
The crux of the technique is a transformation of uninterpreted functions (UFs) applications into integer polynomials, which enables the summarization of loops with UF applications using recurrences. The equivalence checking algorithm then proceeds on loop-free, integer only programs.
We implemented the proposed technique in CORK, a tool that automatically verifies the correctness of compiler optimizations, and we show that it can prove more optimizations correct than state-of-the-art techniques.
N. P. Lopes and J. Monteiro. Automatic Equivalence Checking of UF+IA Programs. In Proc. of the 20th International SPIN Symposium on Model Checking of Software, July 2013 (Best Paper Award).
@inproceedings{cork-spin13,
title = {Automatic Equivalence Checking of {UF+IA} Programs},
author = {Nuno P. Lopes and Jos\'{e} Monteiro},
booktitle = {Proc. of the 20th International SPIN Symposium on Model Checking of Software},
doi = {10.1007/978-3-642-39176-7_18},
month = jul,
year = 2013
}
The final publication is available at link.springer.com.