Solving Constrained Horn Clauses Using Syntax and Data
Solving Constrained Horn Clauses Using Syntax and Data
复制标题
使用语法和数据解决约束 Horn 子句
DOI：
10.23919/fmcad.2018.8603011
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Aarti Gupta
中科院分区：
文献类型：
--
作者：
Grigory Fedyukovich;Sumanth Prabhu;Kumar Madhukar;Aarti Gupta
约束霍恩子句 (CHC) 是涉及未知谓词的逻辑蕴涵。 CHC 系统广泛用于验证具有任意循环结构的程序：对未知谓词的解释，使系统中的每个 CHC 为真，代表程序的归纳不变量。为了找到这样的解决方案，我们提出了一种基于语法引导综合的算法。对于每个未知谓词，它从 CHC 系统的所有相关部分生成形式语法（即使用语法）。从 CHC 系统的各种展开模型（即使用数据）猜测的谓词和常量进一步丰富了语法。我们提出了一种迭代方法来猜测和检查多个未知谓词的候选者。在每次迭代中，仅从其语法中采样一个未知谓词的候选者，但随后通过 CHC 系统中的含义将其传播到其余未知谓词的候选者。最后，使用 SMT 求解器来确定候选系统是否对解决方案有贡献。我们在一系列源自程序验证任务的基准上对该算法进行了评估，并表明它在 CHC 求解方面与最先进的算法具有竞争力。
A Constrained Horn Clause (CHC) is a logical implication involving unknown predicates. Systems of CHCs are widely used to verify programs with arbitrary loop structures: interpretations of unknown predicates, which make every CHC in the system true, represent the program’s inductive invariants. In order to find such solutions, we propose an algorithm based on Syntax-Guided Synthesis. For each unknown predicate, it generates a formal grammar from all relevant parts of the CHC system (i.e., using syntax). Grammars are further enriched by predicates and constants guessed from models of various unrollings of the CHC system (i.e., using data). We propose an iterative approach to guess and check candidates for multiple unknown predicates. At each iteration, only a candidate for one unknown predicate is sampled from its grammar, but then it gets propagated to candidates of the remaining unknowns through implications in the CHC system. Finally, an SMT solver is used to decide if the system of candidates contributes towards a solution or not. We present an evaluation of the algorithm on a range of benchmarks originating from program verification tasks and show that it is competitive with state-of-the-art in CHC solving.