Infinite state model checking by learning transitive relations

DOI10.1007/978-3-031-99984-0_25MaRDI QIDQ6869934zbMATH OpenFDO

Authors Florian Frohn, Jürgen Giesl

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_25

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A calculus for modular loop acceleration
• Automated Technology for Verification and Analysis
• Fast acceleration of ultimately periodic relations
• Global guidance for local generalization in model checking
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• Incremental convex hull algorithms are not output sensitive
• Infinite state model checking by learning transitive relations
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Loop summarization using state and transition invariants
• Loop summarization with rational vector addition systems
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
• Proving safety with trace automata and bounded model checking
• PTIME computation of transitive closures of octagonal relations
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• The \textsc{Golem} Horn solver

Cited in

(1)

• Infinite state model checking by learning transitive relations

This page was built for publication: Infinite state model checking by learning transitive relations

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