Model Checking¶
Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. MIT Press.
Cited by¶
10 citations across 10 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Conjunctive Path Activation
- The remedy is the prime's: not to tighten every signal (defending an OR-failure), but to break the AND at the most robust edge — add a single gate or latch that makes one of the three conditions un-satisfiable in the hazard window — or deploy combination-aware verification (model-checking the state space) rather than per-signal checks.
This sourceFormal verification by exhaustive exploration of a system's state space, catching hazards that single-signal checks miss; addresses the state-explosion problem inherent to inspecting combinations of states.
- The remedy is the prime's: not to tighten every signal (defending an OR-failure), but to break the AND at the most robust edge — add a single gate or latch that makes one of the three conditions un-satisfiable in the hazard window — or deploy combination-aware verification (model-checking the state space) rather than per-signal checks.
- Coverage / Reachability
- Formal verification: every reachable state is enumerated, and unreachability of a bad state is the dual proof obligation.
This sourceStandard text on reachable-state enumeration and reachability analysis in formal verification, including the dual obligation of proving bad states unreachable.
- Formal verification: every reachable state is enumerated, and unreachability of a bad state is the dual proof obligation.
- Decidability Computability
- Engineering verification. Model checking decides safety properties on finite-state models, while theorem proving over richer logics is undecidable, so the same engineered system can be decidable in one specification and undecidable in another.
This sourceEstablishes that safety properties of finite-state models are algorithmically decidable, while verification over richer logics is undecidable.
- Engineering verification. Model checking decides safety properties on finite-state models, while theorem proving over richer logics is undecidable, so the same engineered system can be decidable in one specification and undecidable in another.
- Modal Reasoning
- Model-checking tools mechanize exactly this: they explore the reachable-state space and report whether the invariant holds universally or whether a counterexample trace exists.
This sourceCanonical reference on model checking: mechanizes safety verification as necessity over a reachable-state space, reporting whether an invariant holds universally or returning a counterexample trace witnessing reachability (possibility) of a violating state.
- Model-checking tools mechanize exactly this: they explore the reachable-state space and report whether the invariant holds universally or whether a counterexample trace exists.
- State and State Transition
Domain-specific¶
Mechanisms¶
- Bounded-Domain Exhaustive Search
- Its failure modes are the flip side of brute force: state-space explosion
This sourceIdentifies state-space explosion as the principal practical challenge in exhaustive finite-state model checking.
- Its failure modes are the flip side of brute force: state-space explosion
- Coverage Counterexample Search
- This is falsification applied to coverage: like a model checker, the method earns trust by trying to return a counterexample and failing.
This sourceClarke, Grumberg, and Peled describe model checking as automatic verification that returns a counterexample when a modeled design contains an error.
- This is falsification applied to coverage: like a model checker, the method earns trust by trying to return a counterexample and failing.
- Model Checking and Reachability Analysis
- State-space explosion forces abstraction, and an over-abstracted model can certify a system the real one still breaks.
This sourceExplains that state-space explosion motivates property-preserving abstraction in model checking.
- State-space explosion forces abstraction, and an over-abstracted model can certify a system the real one still breaks.
- State / Action Map
- … characteristic failure is state-space explosion: because states multiply combinatorially with every distinction you add, a map drawn at too fine a grain becomes larger than the problem and stops being usable — the classic misuse is enumerating every micro-configuration until the graph is a hairball no one reads.
This sourceIdentifies state-space explosion as the central model-checking challenge and explains that interacting components and data values can make the number of global states enormous.
- … characteristic failure is state-space explosion: because states multiply combinatorially with every distinction you add, a map drawn at too fine a grain becomes larger than the problem and stops being usable — the classic misuse is enumerating every micro-configuration until the graph is a hairball no one reads.
Verification¶
Does it exist? Confirmed. This work's ISBN resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Not recorded. Neither this nor any other of the 10 citations of this work carries a recorded support check.
Was it audited? Yes. A second, independent pass read the citation against the article text and recorded a verdict.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:c74ea579e0c8 · see in the full table