Ori Lahav

Date: 16:00, Tuesday, May 6, 2014
Speaker: Ori Lahav
Venue: IST Austria

First order logic with transitive closure, and separation logic enable
elegant interactive verification of heap-manipulating programs. However,
undecidabilty results and high asymptotic complexity of checking
validity preclude complete automatic verification of such programs, even
when loop invariants and procedure contracts are specified as formulas
in these logics. We tackle the problem of procedure-modular verification
of reachability properties of heap-manipulating programs using efficient
decision procedures that are complete: that is, a SAT solver must
generate a counterexample whenever a program does not satisfy its
specification. By (a) requiring each procedure modifies a fixed set of
heap partitions and creates a bounded amount of heap sharing, and (b)
restricting program contracts and loop invariants to use only
deterministic paths in the heap, we show that heap reachability updates
can be described in a simple manner. The restrictions force program
specifications and verification conditions to lie within a fragment of
first-order logic with transitive closure that is reducible to
effectively propositional logic, and hence facilitate sound, complete
and efficient verification. We implemented a tool atop Z3 and report on
preliminary experiments that establish the correctness of several
programs that manipulate linked data structures.

Posted in RiSE Seminar