טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentVeitsman Maor
SubjectMethods to Improve completeness of Regression
Verification
DepartmentDepartment of Industrial Engineering and Management
Supervisor Professor Ofer Strichman


Abstract


In this thesis I address the problem of proving the equivalence of two recursive

programs. Specifically we use abstract interpretation to strengthen the premise

of our proof rules and tackle recursive functions which have different base cases

and/or are not in lock-step.

We show a proof rule for the case of different base cases, based on separating

the proof into two parts?inputs which result in the base case in at least one

of the two compared functions, and all the rest. We also show how unbalanced

unrolling of the functions can solve the case in which the functions are not in

lock-step. In itself this type of unrolling may again introduce the problem of the

different base cases, and we show a new proof rule for solving it. None of the

existing software equivalence checkers (like r ? eve , rvt , Symdiff), or general

unbounded software model-checkers (like Seahorn, HSFC, Automizer) can

prove such equivalences.

In addition we use abstract interpretation to help bound the possible outputs

of the uninterpreted functions return values thus improving the completeness

of the proof. We then study an option of using the intersection of the ranges

produced by abstract interpretation for refining the abstraction associated with

uninterpreted functions.