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.
CITATION STYLE
D’Silva, V., & Urban, C. (2015). Conflict-Driven conditional termination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9207, pp. 271–286). Springer Verlag. https://doi.org/10.1007/978-3-319-21668-3_16
Mendeley helps you to discover research relevant for your work.