You are gladly invited to
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.
This work tackles 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 trees and linked lists.
This is a joint work with Shachar Itzhaky and Ori Lahav (Tel Aviv University), Neil Immerman from (UMASS), Anindya Benerjee and Aleksandar Nanevski (IMDEA).
We use automata for software model checking in a new way. The starting point is to fix the alphabet: the set of statements of the given program. We show how automata over the alphabet of statements can help to decompose the main problem in software model checking, which is to find the right abstraction of a program for a given correctness property.
This is a joint work with Matthias Heizmann and Jochen Hoenicke.
Committee:
Last modified: Wed Oct 15 18:52:33 CEST 2014