טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentGodlin Benny
SubjectRegression Verification: Theoretical and Implementation
Aspects
DepartmentDepartment of Computer Science
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

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 un-decidable. There are two main reasons for this claim: it circumvents the problem of specifying what the program should do, and in many cases it is computationally easier. In this thesis we study theoretical and practical aspects of this problem, which we call regression verification.


The thesis is divided into two parts. In the first part we propose several notions of equivalence between programs, and corresponding proof rules in the style of Hoare's rule for recursive procedures. These rules enable us to prove the equivalence of recursive and mutually recursive programs, and also have an advantage from the perspective of the computational effort, since it allows us to decompose and abstract the two programs. This method is sound but incomplete.


In the second part we describe a regression verification tool for C programs, based on the above-mentioned rules, that we built on top of a software bounded model-checker called CBMC.