Program Verification via Predicate Constraint Satisfiability Modulo Theories
Program Verification via Predicate Constraint Satisfiability Modulo Theories
复制标题
通过谓词约束可满足性模理论进行程序验证
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Eric Koskinen
中科院分区：
文献类型：
--
作者：
Hiroshi Unno;Yuki Satake;Tachio Terauchi;Eric Koskinen
本文提出了一种验证框架的基础上一类新的谓词约束满足问题称为pCSP的约束表示为子句模一阶理论的函数变量和谓词变量，可能代表有理有据的谓词。验证框架将现有的基于约束霍恩子句（CHCs）的验证框架推广到任意子句、函数变量和良好基础约束。虽然它是已知的，满足性的CHCs和约束逻辑程序（CLP）的查询的有效性是相互可约的，我们表明，由于增加的表现力，pCSP是表达足够的表达muCLP查询。muCLP本身是我们在本文中提出的CLP的新扩展。它扩展了CLP与任意嵌套的归纳和共归纳谓词，是等价的表达作为一阶不动点逻辑。我们表明，muCLP可以自然地编码各种各样的验证问题，包括但不限于终止/非终止验证，甚至全模态μ演算模型检查的程序编写的各种语言。为了建立我们的验证框架，我们提出了（1）一个健全的和完整的约简算法从muCLP到pCSP和（2）pCSP的约束求解方法的基础上分层反例引导归纳合成（CEGIS）的（共）归纳不变量，排名功能，和Skolem功能见证存在量词。分层CEGIS将CEGIS与分层模板族相结合，通过避免过拟合问题来实现CEGIS的相对完整性和更快、更稳定的收敛。我们已经实施了建议的框架，并取得了可喜的成果，对各种验证问题，超出了以前的验证框架的基础上CHCs的范围。
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo first-order theories over function variables and predicate variables that may represent well-founded predicates. The verification framework generalizes an existing one based on Constrained Horn Clauses (CHCs) to arbitrary clauses, function variables, and well-foundedness constraints. While it is known that the satisfiability of CHCs and the validity of queries for Constrained Logic Programs (CLP) are inter-reducible, we show that, thanks to the added expressiveness, pCSP is expressive enough to express muCLP queries. muCLP itself is a new extension of CLP that we propose in this paper. It extends CLP with arbitrarily nested inductive and co-inductive predicates and is equi-expressive as first-order fixpoint logic. We show that muCLP can naturally encode a wide variety of verification problems including but not limited to termination/non-termination verification and even full modal mu-calculus model checking of programs written in various languages. To establish our verification framework, we present (1) a sound and complete reduction algorithm from muCLP to pCSP and (2) a constraint solving method for pCSP based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of (co-)inductive invariants, ranking functions, and Skolem functions witnessing existential quantifiers. Stratified CEGIS combines CEGIS with stratified families of templates to achieve relative completeness and faster and stable convergence of CEGIS by avoiding the overfitting problem. We have implemented the proposed framework and obtained promising results on diverse verification problems that are beyond the scope of the previous verification frameworks based on CHCs.
用于验证的高阶约束喇叭子句
影响因子：
--
作者：
Cathcart Burn T
通讯作者：
Cathcart Burn T
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
发表时间：
2013
期刊：
影响因子：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko