Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)

DOI10.1007/978-3-031-10769-6_41MaRDI QIDQ2104557zbMATH OpenOpenAlexFDO

Authors Florian Frohn, Jürgen Giesl

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-10769-6_41

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• An LTL proof system for runtime verification
• Proving Non-looping Non-termination Automatically
• Proving Termination of Rewrite Systems Using Bounds
• Verification of a class of loop programs without using loop invariants
• scientific article; zbMATH DE number 4072437
• Termination proofs for ground rewrite systems -- interpretations and derivational complexity
• Verification and falsification of programs with loops using predicate abstraction
• Loop-free verification of termination of derivation for a fragment of dynamic logic

Cites work

• A calculus for modular loop acceleration
• Fast acceleration of ultimately periodic relations
• Iterating Octagons
• Lower runtime bounds for integer programs
• Lower-bound synthesis using loop specialization and Max-SMT
• Under-approximating loops in C programs for fast counterexample detection

Cited in

(3)

• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
• Proving Termination of C Programs with Lists
• LoAT

Describes a project that uses

Uses Software

• FLATA
• PURRS
• StarExec
• TPDB
• GitHub
• iRankFinder

This page was built for publication: Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)

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