Ofer Strichman:
Proving Equivalence of Programs

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 undecidable. 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 talk 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 re-cursive programs, and also has 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.

Bio:
Ofer Stichman's research has concentrated in the last ten years on various aspects of formal verification of software and hardware, including decision procedures for first order theories that are used in program verification, SAT-based model checking, equivalence verification of C programs, and various problems in specification of systems. He also published several works on abstraction/refinement procedures, both for automated theorem proving and for model checking. He recently published a book titled Decision procedures – an algorithmic point of view, coauthored with Daniel Kroening.

Appointments: Contract Dr. Strichman directly at ofers@ie.technion.ac.il

Maintainer [ Home > Seminar ]
`Last modified: Fri Sep 5 11:09:10 EDT 2008