The Birth of Model Checking
From MaRDI portal
Publication:3512430
DOI10.1007/978-3-540-69850-0_1zbMath1142.68046OpenAlexW1577525693MaRDI 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
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) History of computer science (68-03)
Related Items (13)
A linear-time algorithm for the orbit problem over cyclic groups ⋮ Transfer of Model Checking to Industrial Practice ⋮ Data-driven and model-based verification via Bayesian identification and reachability analysis ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Linear temporal logic symbolic model checking ⋮ Static analysis and stochastic search for reachability problem ⋮ Safety preserving control synthesis for sampled data systems ⋮ Logical classification of distributed algorithms (Bakery algorithms as an example) ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey ⋮ Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
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
This page was built for publication: The Birth of Model Checking
