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

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:20
25m
Talk
Learning Programs from Noisy Data
Research Papers
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45
25m
Talk
Optimizing Synthesis with Metasketches
Research Papers
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USA
Pre-print Media Attached
15:10
25m
Talk
Maximal Specification Synthesis
Research Papers
Aws Albarghouthi University of Wisconsin–Madison, Isil Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon University
Pre-print Media Attached
15:35
25m
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
Pre-print Media Attached File Attached