Proving Non-Termination by Acceleration Driven Clause Learning

arXiv (Cornell University)

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 LoAT and evaluate it against the state of the art.

Authors 2

1. Florian Frohn Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Aachen , Germany

2. Jürgen Giesl Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Aachen , Germany