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

DOI10.1007/978-3-031-38499-8_13MaRDI QIDQ6492742zbMATH OpenFDO

Authors Florian Frohn, Jürgen Giesl

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_13

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A calculus for modular loop acceleration
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Geometric nontermination arguments
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• Iterating Octagons
• Loop detection by logically constrained term rewriting
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Proving termination through conditional termination

Cited in

(2)

• Infinite state model checking by learning transitive relations
• Satisfiability modulo exponential integer arithmetic

This page was built for publication: Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492742)