Optimal CHC Solving via Termination Proofs
Optimal CHC Solving via Termination Proofs
复制标题
通过终止证明最优 CHC 求解
DOI：
10.1145/3571214
复制
发表时间：
2023
影响因子：
--
通讯作者：
Unno Hiroshi
中科院分区：
文献类型：
--
作者：
Gu Yu;Tsukada Takeshi;Unno Hiroshi
受开放式程序推理（如最大规格推理）应用的启发，本文研究了最优CHC求解问题，即计算约束Horn子句（CHC）的最大和/或最小解的问题。这个问题及其子问题已经在文献中进行了研究，一个主要的方法是迭代改进CHCs的解决方案，直到它成为最优的。因此，优化方法的一个关键组成部分是给定解决方案的最优性检查。我们提出了一种新的最优性检查方法，以及使用建议的最优性检查器的优化方法，基于计算理论分析的最优性检查问题。关键的观察是，最优性检查问题是密切相关的程序的终止性分析，这一观察是有用的理论和实践。从理论上阐明了现有方法的局限性和文献中另一种方法的不正确性。从实际的角度来看，它使我们能够应用技术的终止分析的CHCs的解决方案的最优性检查。我们提出了一种基于约束的终止参数合成的最优性检查方法，实现了我们的方法，评估它对编码最大规格合成问题的CHCs，并取得了可喜的成果。
Motivated by applications to open program reasoning such as maximal specification inference, this paper studiesoptimal CHC solving, a problem to compute maximal and/or minimal solutions of constrained Horn clauses (CHCs). This problem and its subproblems have been studied in the literature, and a major approach is to iteratively improve a solution of CHCs until it becomes optimal. So a key ingredient of optimization methods is the optimality checking of a given solution. We propose a novel optimality checking method, as well as an optimization method using the proposed optimality checker, based on a computational theoretical analysis of the optimality checking problem. The key observation is that the optimality checking problem is closely related to the termination analysis of programs, and this observation is useful both theoretically and practically. From a theoretical perspective, it clarifies a limitation of an existing method and incorrectness of another method in the literature. From a practical perspective, it allows us to apply techniques of termination analysis to the optimality checking of a solution of CHCs. We present an optimality checking method based on constraint-based synthesis of termination arguments, implemented our method, evaluated it on CHCs that encode maximal specification synthesis problems, and obtained promising results.
登录
查看更多内容
具有约束 Horn 子句的规范综合
DOI：
10.1145/3453483.3454104
发表时间：
2021
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Sumanth Prabhu;Grigory Fedyukovich;Kumar Madhukar;D. D'Souza
通讯作者：
D. D'Souza
影响因子：
--
作者：
Zhe Zhou;R. Dickerson;Benjamin Delaware;S. Jagannathan
通讯作者：
Zhe Zhou;R. Dickerson;Benjamin Delaware;S. Jagannathan
基于 CEGIS 的终止分析中的决策树学习
DOI：
10.1007/978-3-030-81688-9_4
发表时间：
2021
期刊：
Proceedings of CAV 2021, Springer LNCS
影响因子：
--
作者：
Kura Satoshi;Unno Hiroshi;Hasuo Ichiro
通讯作者：
Hasuo Ichiro
几乎正确的规范：用于为警告分配置信度的模块化语义框架
DOI：
10.1145/2491956.2462188
发表时间：
2013
期刊：
ACM-SIGPLAN Symposium on Programming Language Design and Implementation
影响因子：
--
作者：
Sam Blackshear;Shuvendu K. Lahiri
通讯作者：
Shuvendu K. Lahiri
通过树学习动态推断谓词上可能的数据先决条件
影响因子：
0.8
作者：
S. Sankaranarayanan;Swarat Chaudhuri;Franjo Ivancic;Aarti Gupta
通讯作者：
Aarti Gupta