Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)

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 disprove termination of transition systems, and we evaluate its implementation in our tool LoAT 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