Solving Horn Clauses on Inductive Data Types Without Induction
Solving Horn Clauses on Inductive Data Types Without Induction
复制标题
DOI：
10.1017/s1471068418000157
复制
发表时间：
2018-07-01
影响因子：
1.4
通讯作者：
Proietti, Maurizio
中科院分区：
文献类型：
--
作者：
De Angelis, Emanuele;Fioravanti, Fabio;Proietti, Maurizio
基于归纳定义的数据结构理论，如列表和树，我们研究了约束Horn子句(CHC)的可满足性验证问题。我们提出了一种变换技术，其目标是将这些数据结构从CHC中移除，从而将它们的可满足性归结为CHC关于整数和布尔的可满足性问题。我们提出了一种转换算法，并找出了一类它总是成功的子句。我们还考虑了该算法的扩展，它结合了子句转换和对整数约束的推理。通过实验评估，我们的技术极大地提高了将Z3求解器应用于CHC的有效性。我们还表明，我们的基于CHC变换和CHC求解的验证技术相对于通过归纳扩展的CHC求解器是有竞争力的。
We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.