Regression verification: proving the equivalence of similar programs

摘要

Proving the equivalence of successive, closely related versions of a program has the potential of being easier in practice than functional verification, although both problems are undecidable. There are three main reasons for this claim: (i) it circumvents the problem of specifying what the program should do; (ii) the problem can be naturally decomposed and hence is computationally easier; and (iii) there is an automatic invariant that enables to prove equivalence of loops and recursive functions in most practical cases. Theoretical and practical aspects of this problem are considered.