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

DOI10.1007/978-3-031-10769-6_41OpenAlexW4289104025MaRDI QIDQ2104557FDOQ2104557

Authors: Florian Frohn, Jürgen Giesl 

Publication date: 7 December 2022

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

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

Mathematics Subject Classification ID

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

Cites Work

• Fast acceleration of ultimately periodic relations
• Iterating Octagons
• Under-approximating loops in C programs for fast counterexample detection
• Lower Runtime Bounds for Integer Programs
• A Calculus for Modular Loop Acceleration
• Lower-bound synthesis using loop specialization and Max-SMT

Cited In (3)

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

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)