Conflict-Driven Conditional Termination

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.

Publication
In Proc. 25th International Conference on Computer Aided Verification (CAV 2015)
Date

FuncTion