The Birth of Model Checking

DOI10.1007/978-3-540-69850-0_1zbMATH Open1142.68046OpenAlexW1577525693MaRDI QIDQ3512430FDOQ3512430

Authors: Edmund Clarke 

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

Recommendations

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

zbMATH Keywords

model checkinghistoryfuture perspectives

Mathematics Subject Classification ID

History of computer science (68-03) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• NuSMV: A new symbolic model checker
• Characterizing finite Kripke structures in propositional temporal logic
• Title not available (Why is that?)
• Reasoning about networks with many identical finite state processes
• Learning regular sets from queries and counterexamples
• Symbolic model checking: \(10^{20}\) states and beyond
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of propositional linear temporal logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computer Aided Verification
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Verifying properties of parallel programs
• Soundness and Completeness of an Axiom System for Program Verification
• Results on the propositional \(\mu\)-calculus
• “Sometimes” and “not never” revisited
• Title not available (Why is that?)
• The temporal logic of branching time
• On the completeness of the inductive assertion method
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reachability analysis of pushdown automata: Application to model-checking
• Title not available (Why is that?)
• Proofs of Networks of Processes
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Inference of finite automata using homing sequences
• Monotone data flow analysis frameworks
• Proving Liveness Properties of Concurrent Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• LAR: A logic of algorithmic reasoning
• Title not available (Why is that?)
• Program invariants as fixedpoints
• Effective Axiomatizations of Hoare Logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic Verification of Sequential Circuits Using Temporal Logic
• Title not available (Why is that?)
• Computer Aided Verification
• FM 2005: Formal Methods
• Computer aided verification. 5th international conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
• Title not available (Why is that?)
• Hierarchical verification of asynchronous circuits using temporal logic
• Hardware Specification with Temporal Logic: An Example
• Proving correctness of coroutines without history variables
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Anomaly Detection in Concurrent Software by Static Data Flow Analysis
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (16)

• Constraint-based debugging in probabilistic model checking
• Minimal counterexamples for linear-time probabilistic verification
• Data-driven and model-based verification via Bayesian identification and reachability analysis
• Logical classification of distributed algorithms (Bakery algorithms as an example)
• Counterexample generation for discrete-time Markov models: an introductory survey
• 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
• A linear-time algorithm for the orbit problem over cyclic groups
• Safety preserving control synthesis for sampled data systems
• Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
• Static analysis and stochastic search for reachability problem
• Linear temporal logic symbolic model checking
• From EU projects to a family of model checkers. From Kandinsky to KandISTI
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• Transfer of Model Checking to Industrial Practice
• The Beginning of Model Checking: A Personal Perspective

Uses Software

• NuSMV

This page was built for publication: The Birth of Model Checking

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