Tag
model-checking
- Sep 30, 2026 Litmus Tests as Executable Specifications How a five-line concurrency test becomes a machine-checkable claim, what the litmus file format encodes, and how a model checker decides which outcomes are forbidden. memory systems
- Aug 26, 2026 Exhaustive State Exploration and What a Bounded Model Proves How model checking enumerates reachable states, why a bound is a parameter of the claim rather than a shortcut, and how to read a counterexample as a requirement defect. software engineering
- Aug 12, 2026 Verifying Crash Consistency with Fault Injection Why a crash-consistency claim needs an exhaustive state-space argument rather than a test, how to model a device that loses writes and reorders them, and which failures the method cannot find. memory systems
- Jul 24, 2026 Litmus Tests and How Allowed Outcomes Are Decided How a few lines of concurrent code pin down a memory model, how tools enumerate the executions, and why "never observed" is weaker than "forbidden". computer architecture