Meanings of model checking

DOI10.1007/978-3-642-11512-7_15MaRDI QIDQ5187832zbMATH OpenOpenAlexFDO

Authors E. Allen Emerson

Publication date 9 March 2010

Published in Concurrency, Compositionality, and Correctness (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11512-7_15

zbMATH Keywords

model checkingalternative definitionsspecial applications

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Introduction to model checking
• scientific article; zbMATH DE number 1487860
• The Beginning of Model Checking: A Personal Perspective
• scientific article; zbMATH DE number 910719
• Model checking

Cites work

• scientific article; zbMATH DE number 1670793 (Why is no real title available?)
• scientific article; zbMATH DE number 1701775 (Why is no real title available?)
• scientific article; zbMATH DE number 1705164 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 177509 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3624762 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 3271460 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• A deterministic subexponential algorithm for solving parity games
• A lattice-theoretical fixpoint theorem and its applications
• A logic for reasoning about time and reliability
• An axiomatic basis for computer programming
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Concurrency verification. Introduction to compositional and noncompositional methods
• Graph-Based Algorithms for Boolean Function Manipulation
• Modalities for model checking: Branching time logic strikes back
• Model checking contractual protocols
• On Computable Numbers, with an Application to the Entscheidungsproblem
• Proceedings of the 7th international workshop on parallel and distributed methods in verification (PDMC 2008), Budapest, Hungary, March 29, 2008.
• Program invariants as fixedpoints
• Results on the propositional \(\mu\)-calculus
• The temporal logic of branching time
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• “Sometimes” and “not never” revisited

Cited in

(1)

• The Birth of Model Checking

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Meanings of model checking

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