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
|14:20 - 14:45|
Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH ZurichLink to publication DOI Pre-print Media Attached File Attached
|14:45 - 15:10|
James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USAPre-print Media Attached
|15:10 - 15:35|
Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon UniversityPre-print Media Attached
|15:35 - 16:00|
Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of PennsylvaniaPre-print Media Attached File Attached