Conflict-Driven Conditional Termination

Vijay d'Silva (1) , Caterina Urban (2)

1 Google Inc [Mountain View]
2 DI-ENS - Département d'informatique - ENS Paris

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.

Domaines: Logique en informatique [cs.LO]

Vijay d'Silva, Caterina Urban. Conflict-Driven Conditional Termination. 25th International Conference on Computer Aided Verification (CAV 2015), 2015, San Francisco, United States. ⟨hal-01952911⟩