Regression Verification: Proving the Equivalence of Similar Programs

The ability to prove equivalence of successive, closely-related versions of a program can be useful for maintaining backward compatibility. This problem has the potential of being easier in practice than functional verification for at least two reasons: First, it circumvents the problem of specifying what the program should do; Second, in many cases it is computationally easier, because it offers various opportunities for abstraction and decomposition that are only relevant in this context.

I will begin the talk by defining six notions of input/output equivalence between programs, and then show Hoare-style proof rules that can be used for proving the equivalence of recursive functions according to these definitions. I will then show a decomposition algorithm that, given a mapping between the recursive functions in the two programs, attempts to reduce the equivalence verification problem into verification of many smaller verification problems corresponding to pairs of mapped functions. Callees of these functions that were already proven equivalent are abstracted with uninterpreted functions. I will conclude the talk by describing a regression verification tool for C programs – built by Benny Godlin – that, based on these rules and decomposition algorithm, was able to prove automatically the equivalence of some nontrivial programs.

This is a joint work with Benny Godlin. The same talk was given as an invited talk in CAV’09.

Speaker Details

Ofer Strichman is active in the formal verification arena for over 10 years. He earned his PhD from the Weizmann institute of Science in 2001, under the supervision of Amir Pnueli. He published over 60 articles in formal verification and a book on decision procedures. His research interests include decision procedures for first-order theories, model-checking and software equivalence checking. He is currently an associate professor in the Technion, Haifa, Israel.

Ofer Strichman
Technion, Haifa, Israel