Regression Verification: Proving the Equivalence of Similar Programs

(Invited Talk)
  • Ofer Strichman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


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.


  1. [GS08]
    Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6), 403–439 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  2. [GS09]
    Godlin, B., Strichman, O.: Regression verification. In: 46th Design Automation Conference (DAC) (2009) (to be published)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ofer Strichman
    • 1
  1. 1.Information Systems Engineering, IE, TechnionHaifaIsrael

Personalised recommendations