The Birth of Model Checking
From MaRDI portal
Publication:3512430
DOI10.1007/978-3-540-69850-0_1zbMath1142.68046MaRDI QIDQ3512430
Publication date: 15 July 2008
Published in: 25 Years of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-69850-0_1
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B44: Temporal logic
68-03: History of computer science
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The temporal logic of branching time
- Results on the propositional \(\mu\)-calculus
- Reasoning about networks with many identical finite state processes
- Hierarchical verification of asynchronous circuits using temporal logic
- Learning regular sets from queries and counterexamples
- Characterizing finite Kripke structures in propositional temporal logic
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Symbolic model checking: \(10^{20}\) states and beyond
- LAR: A logic of algorithmic reasoning
- On the completeness of the inductive assertion method
- Monotone data flow analysis frameworks
- Program invariants as fixedpoints
- Proving correctness of coroutines without history variables
- Computer aided verification. 5th international conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
- NuSMV: A new symbolic model checker
- Inference of finite automata using homing sequences
- A lattice-theoretical fixpoint theorem and its applications
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Effective Axiomatizations of Hoare Logics
- “Sometimes” and “not never” revisited
- The complexity of propositional linear temporal logics
- Anomaly Detection in Concurrent Software by Static Data Flow Analysis
- Proofs of Networks of Processes
- Hardware Specification with Temporal Logic: An Example
- Proving Liveness Properties of Concurrent Programs
- Verifying properties of parallel programs
- Soundness and Completeness of an Axiom System for Program Verification
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Computer Aided Verification
- Computer Aided Verification
- FM 2005: Formal Methods
- Reachability analysis of pushdown automata: Application to model-checking
