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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00
|Learning Programs from Noisy Data
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH ZurichLink to publication DOI Pre-print Media Attached File Attached
|Optimizing Synthesis with Metasketches
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USAPre-print Media Attached
|Maximal Specification Synthesis
Aws Albarghouthi University of Wisconsin–Madison, Işıl Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon UniversityPre-print Media Attached
|Example-Directed Synthesis: A Type-Theoretic Interpretation
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of PennsylvaniaPre-print Media Attached File Attached