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.
- [GS09]Godlin, B., Strichman, O.: Regression verification. In: 46th Design Automation Conference (DAC) (2009) (to be published)Google Scholar