Specification synthesis with constrained Horn clauses
Specification synthesis with constrained Horn clauses
复制标题
具有约束 Horn 子句的规范综合
DOI：
10.1145/3453483.3454104
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
D. D'Souza
中科院分区：
文献类型：
--
作者：
Sumanth Prabhu;Grigory Fedyukovich;Kumar Madhukar;D. D'Souza
不确定程序的合成规格的问题具有广泛的应用，但是生成规格的有用性取决于其质量。在本文中，我们提出了一种用于查找最大和不变规范的技术。最大程度可以为实施未定义的程序做出更多选择，而非现象可确保可以达成安全主张。为了处理具有复杂控制流程的程序，我们的技术不仅发现规格，还会发现电感不变性。我们的迭代算法懒洋洋地概括了反例引导环中的非呈现规格。我们技术的关键组成部分是一种有效的非散布规范合成算法。我们已经在称为HornSpec的工具中实现了该方法，将其作为约束喇叭子句的输入系统。我们通过实验证明了该工具在一系列基准上的有效性，效率和生成规格的质量。
The problem of synthesizing specifications of undefined procedures has a broad range of applications, but the usefulness of the generated specifications depends on their quality. In this paper, we propose a technique for finding maximal and non-vacuous specifications. Maximality allows for more choices for implementations of undefined procedures, and non-vacuity ensures that safety assertions are reachable. To handle programs with complex control flow, our technique discovers not only specifications but also inductive invariants. Our iterative algorithm lazily generalizes non-vacuous specifications in a counterexample-guided loop. The key component of our technique is an effective non-vacuous specification synthesis algorithm. We have implemented the approach in a tool called HornSpec, taking as input systems of constrained Horn clauses. We have experimentally demonstrated the tool's effectiveness, efficiency, and the quality of generated specifications on a range of benchmarks.