Proving Non-Termination by Acceleration Driven Clause Learning

Autor:	Frohn, Florian, Giesl, Jürgen
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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.
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2304.10166 Zobrazit plný text záznamu View this record from Arxiv