Solving Recursion-Free Horn Clauses over LI+UIF
Solving Recursion-Free Horn Clauses over LI+UIF
复制标题
通过 LI UIF 求解无递归 Horn 子句
DOI：
10.1007/978-3-642-25318-8_16
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Andrey Rybalchenko
中科院分区：
文献类型：
--
作者：
Ashutosh Gupta;Corneliu Popeea;Andrey Rybalchenko
使用依赖于用于抽象发现的虚假反例的抽象和精化方案，可以有效地自动化对具有过程的程序、多线程程序和高阶函数程序的验证。反例的分析可以通过一系列内插查询来自动化，或者，作为替代，作为由一组递归的自由Horn子句表示的约束求解查询。(一组内插查询可以表示为在未知关系之间具有线性依赖结构的Horn子句上的单个约束。)在这篇文章中，我们给出了一个在线性实数/有理算术和未解释函数的组合理论上求解无递归Horn子句的算法。我们的算法执行归结来处理子句结构，并依赖部分解来处理功能公理的(非局部)实例。
Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively automated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexamples can be automated by a series of interpolation queries, or, alternatively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolution to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.
登录
查看更多内容
内插无量词 Presburger 算法
DOI：
--
发表时间：
2010
期刊：
Logic Programming and Automated Reasoning
影响因子：
--
作者：
D. Kroening;Jérôme Leroux;Philipp Rümmer
通讯作者：
Philipp Rümmer
MathSAT 4SMT 求解器
DOI：
--
发表时间：
2008
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Roberto Bruttomesso;A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani
通讯作者：
R. Sebastiani
影响因子：
0.5
作者：
Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
通讯作者：
Sebastiani, Roberto
无量词 Presburger 算术的插值顺序微积分
DOI：
10.1007/s10817-011-9237-y
发表时间：
2010
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Angelo Brillout;D. Kroening;Philipp Rümmer;T. Wahl
通讯作者：
T. Wahl
DOI：
10.1007/978-3-540-70545-1_29
发表时间：
2008-07
期刊：
--
影响因子：
--
作者：
Dirk Beyer;D. Zufferey;R. Majumdar
通讯作者：
Dirk Beyer;D. Zufferey;R. Majumdar