TLA+ Model Checking Made Symbolic

Created on 2022-02-17T15:04:37-06:00

Paper has pretty typeface and layout.
TLA+ is typically checked by running TLC.
TLC works by iterating all possible states of the specification which is slow.
Converts a subset of TLA+ to something which can then be solved with SMT solvers.
Important because SMT solvers are faster than TLC.
TODO come back and read this at some point.