Induction in compositional model checking

DOI10.1007/10722167_25MaRDI QIDQ2754093zbMATH OpenFDO

Authors K. L. McMillan, James B. Saxe, Shaz Qadeer

Publication date 17 December 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722167_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 910719
• Compositionality and locality for improving model checking in the selective mu-calculus
• Certifying model checkers
• Abstract patterns of compositional reasoning.
• From model checking to a temporal proof

Cited in

(8)

• SAT-based induction for temporal safety properties
• Automated formal analysis and verification: an overview
• An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets
• Automatic Synthesis of Assumptions for Compositional Model Checking
• On Extending Bounded Proofs to Inductive Proofs
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Checking Sufficient Completeness by Inductive Theorem Proving
• An automatic abstraction technique for verifying featured, parameterised systems

Describes a project that uses

Uses Software

• Cadence SMV

This page was built for publication: Induction in compositional model checking

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