The Birth of Model Checking
From MaRDI portal
Publication:3512430
Recommendations
Cites work
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3926220 (Why is no real title available?)
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- scientific article; zbMATH DE number 4047662 (Why is no real title available?)
- scientific article; zbMATH DE number 3651705 (Why is no real title available?)
- scientific article; zbMATH DE number 3714896 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 177237 (Why is no real title available?)
- scientific article; zbMATH DE number 177240 (Why is no real title available?)
- scientific article; zbMATH DE number 177254 (Why is no real title available?)
- scientific article; zbMATH DE number 177500 (Why is no real title available?)
- scientific article; zbMATH DE number 177503 (Why is no real title available?)
- scientific article; zbMATH DE number 3469999 (Why is no real title available?)
- scientific article; zbMATH DE number 3485178 (Why is no real title available?)
- scientific article; zbMATH DE number 3624762 (Why is no real title available?)
- scientific article; zbMATH DE number 1263213 (Why is no real title available?)
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- scientific article; zbMATH DE number 1956591 (Why is no real title available?)
- scientific article; zbMATH DE number 3993457 (Why is no real title available?)
- scientific article; zbMATH DE number 4119616 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- A lattice-theoretical fixpoint theorem and its applications
- Anomaly Detection in Concurrent Software by Static Data Flow Analysis
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Characterizing finite Kripke structures in propositional temporal logic
- Computer Aided Verification
- Computer Aided Verification
- Computer aided verification. 5th international conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
- Effective Axiomatizations of Hoare Logics
- FM 2005: Formal Methods
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Hardware Specification with Temporal Logic: An Example
- Hierarchical verification of asynchronous circuits using temporal logic
- Inference of finite automata using homing sequences
- LAR: A logic of algorithmic reasoning
- Learning regular sets from queries and counterexamples
- Monotone data flow analysis frameworks
- NuSMV: A new symbolic model checker
- On the completeness of the inductive assertion method
- Program invariants as fixedpoints
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Proofs of Networks of Processes
- Proving Liveness Properties of Concurrent Programs
- Proving correctness of coroutines without history variables
- Reachability analysis of pushdown automata: Application to model-checking
- Reasoning about networks with many identical finite state processes
- Results on the propositional \(\mu\)-calculus
- Soundness and Completeness of an Axiom System for Program Verification
- Symbolic model checking: \(10^{20}\) states and beyond
- The complexity of propositional linear temporal logics
- The temporal logic of branching time
- Verifying properties of parallel programs
- “Sometimes” and “not never” revisited
Cited in
(16)- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- Linear temporal logic symbolic model checking
- Logical classification of distributed algorithms (Bakery algorithms as an example)
- Static analysis and stochastic search for reachability problem
- Transfer of model checking to industrial practice
- Minimal counterexamples for linear-time probabilistic verification
- Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
- Safety preserving control synthesis for sampled data systems
- A linear-time algorithm for the orbit problem over cyclic groups
- The Beginning of Model Checking: A Personal Perspective
- A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
- Data-driven and model-based verification via Bayesian identification and reachability analysis
- From EU projects to a family of model checkers. From Kandinsky to KandISTI
- Constraint-based debugging in probabilistic model checking
- 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
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)
