|
|
|
|
|
|
by sriram_malhar
1707 days ago
|
|
|
Very nicely written. In addition, the example chosen was itself lovely to play with. Explicit-state model checkers do this at scale. Readers may be interested in the internals of the TLA+ model checker, esp. the encoding of the state and dealing with disk. Model Checking TLA+ Specifications by Yuan Yu, Panagiotis Manolios, and Leslie Lamport (1999) https://lamport.azurewebsites.net/pubs/yuanyu-model-checking... |
|
|