Maximal Specification Synthesis
ACM SIGPLAN Notices(2016)
摘要
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 phi and a program P calling a set of unknown procedures F-1, . . . , F-n, what are the most permissive specifications of procedures F-i 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 F-i 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 routines invoked by device drivers.
更多查看译文
关键词
verification,specification,synthesis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络