Conflict-Driven Conditional Termination
Conflict-Driven Conditional Termination
复制标题
冲突驱动的有条件终止
DOI：
10.1007/978-3-319-21668-3_16
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Caterina Urban
中科院分区：
文献类型：
--
作者：
V. D'Silva;Caterina Urban
冲突驱动学习对sat和smt求解器的性能至关重要，它包括一个搜索公式模型的过程，以及证明不存在模型的反驳过程。研究表明，冲突驱动学习可以提高基于抽象解释的终止分析的精度。我们将一元二阶逻辑中的非终止性编码为可满足性，并使用抽象解释器对该公式的可满足性进行了推理。我们的搜索程序结合了决策和可达性分析，以发现潜在的非终止执行，我们的反驳程序使用条件终止分析。我们的实现扩展了由现有终止分析器发现的条件终止参数集。
Conflict-driven learning, which is essential to the performance of sat and smt solvers, consists of a procedure that searches for a model of a formula, and refutation procedure for proving that no model exists. This paper shows that conflict-driven learning can improve the precision of a termination analysis based on abstract interpretation. We encode non-termination as satisfiability in a monadic second-order logic and use abstract interpreters to reason about the satisfiability of this formula. Our search procedure combines decisions with reachability analysis to find potentially non-terminating executions and our refutation procedure uses a conditional termination analysis. Our implementation extends the set of conditional termination arguments discovered by an existing termination analyzer.
DOI：
10.1145/2737924.2737993
发表时间：
2015-06
期刊：
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
T. Le;S. Qin;W. Chin
通讯作者：
T. Le;S. Qin;W. Chin
影响因子：
0.8
作者：
Brain, Martin;D'Silva, Vijay;Kroening, Daniel
通讯作者：
Kroening, Daniel
抽象冲突驱动学习
DOI：
10.1145/2429069.2429087
发表时间：
2013
期刊：
--
影响因子：
--
作者：
D'Silva V
通讯作者：
D'Silva V