Certifying rlive: a new proof strategy for liveness model checking

DOI10.1007/978-3-032-04167-8_21MaRDI QIDQ6852299zbMATH OpenFDO

Authors Giulia Sindoni, Alberto Griggio, Stefano Tonetta

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-04167-8_21

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Proof System for the Linear Time μ-Calculus
• An automata-theoretic approach to linear temporal logic
• Certifying model checkers
• Certifying phase abstraction
• Certifying proofs for SAT-based model checking
• From complementation to certification
• From falsification to verification
• From model checking to a temporal proof
• Progress in certifying hardware model checking results

This page was built for publication: Certifying rlive: a new proof strategy for liveness model checking

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