Solving Existentially Quantified Horn Clauses
Solving Existentially Quantified Horn Clauses
复制标题
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Andrey Rybalchenko
中科院分区：
文献类型：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
各种程序（例如程序、多线程或函数）的通用（即对所有计算路径有效）属性的时间验证可以简化为以普遍量化的霍恩子句的形式寻找方程的解，并用有充分根据的条件进行扩展。然而，处理存在性属性（例如，是否存在特定的计算路径）需要求解所有存在的量化 Horn 子句，其中某些子句的结论部分包含存在性量化变量。例如，CTL 验证的演绎方法可以简化为解决此类子句。在本文中，我们提出了一种解决所有存在的量化 Horn 子句的方法，该子句在有充分根据的条件下扩展。我们的方法基于反例引导的抽象细化方案来发现存在量化变量的证据。我们还介绍了我们的求解方法在软件 CTL 验证自动化及其实验评估中的应用。
Temporal verification of universal (i.e., valid for all computation paths) properties of various kinds of programs, e.g., procedural, multi-threaded, or functional, can be reduced to finding solutions for equations in form of universally quantified Horn clauses extended with well-foundedness conditions. Dealing with existential properties (e.g., whether there exists a particular computation path), however, requires solving forall-exists quantified Horn clauses, where the conclusion part of some clauses contains existentially quantified variables. For example, a deductive approach to CTL verification reduces to solving such clauses. In this paper we present a method for solving forall-exists quantified Horn clauses extended with well-foundedness conditions. Our method is based on a counterexample-guided abstraction refinement scheme to discover witnesses for existentially quantified variables. We also present an application of our solving method to automation of CTL verification of software, as well as its experimental evaluation.
登录
查看更多内容
MathSAT 4SMT 求解器
DOI：
--
发表时间：
2008
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Roberto Bruttomesso;A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani
通讯作者：
R. Sebastiani
从测试到证明
DOI：
10.1007/s10009-012-0267-5
发表时间：
2013
影响因子：
1.5
作者：
Ashutosh Gupta;Rupak Majumdar;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko
正在考虑在逻辑编程的理论与实践中发表无限状态系统验证的泛化策略
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
F. Fioravanti;A. Pettorossi;M. Proietti;V. Senni
通讯作者：
V. Senni
DOI：
--
发表时间：
1998
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
C. Palamidessi;H. Glaser;K. Meinke
通讯作者：
K. Meinke
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
K. McMillan;A. Rybalchenko
通讯作者：
A. Rybalchenko