Model checking¶
Category: Testing and tools · Status: stub · Lessons: chapter 09, Testing and tools (planned)
One line: Exploring every state and interleaving of a model of a program — in TLA+, SPIN, or loom — to prove a property or produce a counterexample.
Also called: TLA+, SPIN, Lincheck.
How it connects¶
- See also: Deterministic scheduling for tests
In each language¶
| Rust | loom ↗ simulates the operating system's scheduler and Rust's memory model so that all possible valid behaviours are explored |
| Kotlin | Lincheck ↗ model checking inserts thread switches at synchronization points and shared memory accesses, and reports an exact failing trace |
| Elsewhere | TLA+ ↗ models concurrent and distributed systems; Spin ↗ formally verifies multi-threaded software |
Where to read more¶
- In the books: The Art of Concurrency, Clay Breshears — ch. 3, 'Proving Correctness and Measuring Performance'
- Reference: Wikipedia: Model checking ↗