Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
Florian Frohn, Jürgen Giesl · Lecture notes in computer science · 2023
Abstract We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition systems and introduce ADCL-NT, a variant for disproving termination. We implemented ADCL-NT in our tool and evaluate it against the state of the art.