**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.