Write a Blog >>
Fri 22 Jan 2016 15:10 - 15:35 at Grand Bay North - Track 1: Synthesis Chair(s): Roberto Giacobazzi

Many problems in program analysis, verification, and synthesis require inferring specifications of unknown procedures. Motivated by a broad range of applications, we formulate the problem of maximal specification inference: Given a postcondition φ and a program P calling a set of unknown procedures F1 , … , Fn , what are the most permissive specifications of procedures Fi that ensure correctness of P? In other words, we are looking for the smallest number of assumptions we need to make about the behaviours of Fi in order to prove that P satisfies its postcondition.

To solve this problem, we present a novel approach that utilizes a counterexample-guided inductive synthesis loop and reduces the maximal specification inference problem to multi-abduction. We formulate the novel notion of multi-abduction as a generalization of classical logical abduction and present an algorithm for solving multi-abduction problems. On the practical side, we evaluate our specification inference technique on a range of benchmarks and demonstrate its ability to synthesize specifications of kernel rou- tines invoked by device drivers.

Fri 22 Jan
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Research Papers - Track 1: Synthesis at Grand Bay North
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
POPL-2016-papers14:20 - 14:45
Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
POPL-2016-papers14:45 - 15:10
James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USA
Pre-print Media Attached
POPL-2016-papers15:10 - 15:35
Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon University
Pre-print Media Attached
POPL-2016-papers15:35 - 16:00
Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
Pre-print Media Attached File Attached