MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Ori Lahav
Tel Aviv University
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Thursday, 24 April 2014
10:30
60 Minutes
G26
113
Kaiserslautern

Abstract

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.

Presented in POPL'14.

Joint work with:
Shachar Itzhaky (Tel Aviv University), Anindya Banerjee (IMDEA Software Institute), Neil Immerman (University of Massachusetts), Aleksandar Nanevski (IMDEA Software Institute), Mooly Sagiv (Tel Aviv University)

Contact

--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only

Vera Laubscher, 04/23/2014 11:11 -- Created document.