TLA+ Model Checking Made Symbolic

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

Return to the Index

This card pertains to a resource available on the internet.

• 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.