Conflict-Driven Conditional Termination
Venue
Computer Aided Verification, Springer International Publishing (2015), pp. 271-286
Publication Year
2015
Authors
Vijay D'Silva, Caterina Urban
BibTeX
Abstract
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.
