Model checking as program verification by abstract interpretation

DOI10.4230/LIPICS.CONCUR.2025.8MaRDI QIDQ7310278zbMATH OpenFDO

Authors Paolo Baldan, Roberto Bruni, Francesco Ranzato, Diletta Rigo

Publication date 5 August 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2025.8

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A correctness and incorrectness program logic
• Abstraction and abstraction refinement
• Computer Aided Verification
• Computer Aided Verification
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• Counterexample-guided abstraction refinement for symbolic model checking
• Data flow analysis as model checking
• Fixpoint-Guided Abstraction Refinements
• Generalized Strong Preservation by Abstract Interpretation
• Generating data flow analysis algorithms from modal specifications
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1692938 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 408802 (Why is no real title available?)
• scientific article; zbMATH DE number 1948410 (Why is no real title available?)
• scientific article; zbMATH DE number 1948411 (Why is no real title available?)
• scientific article; zbMATH DE number 1953280 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 2143089 (Why is no real title available?)
• scientific article; zbMATH DE number 1834576 (Why is no real title available?)
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• Incompleteness of states w.r.t. traces in model checking
• Making abstract interpretations complete
• Model checking
• Model checking \textit{is} static analysis of modal logic
• Predicate abstraction for program verification
• Principles of abstract interpretation
• Property preserving abstractions for the verification of concurrent systems
• Simulation-based minimization
• Software model checking
• Temporal abstract interpretation
• Temporal logic can be more expressive
• Tools and Algorithms for the Construction and Analysis of Systems
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus

This page was built for publication: Model checking as program verification by abstract interpretation

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