Apalache
Formal verification · a symbolic model checker
created · updated
A program that checks models written in TLA+ and Quint. It turns them into a set of conditions and hands them to an SMT solver, for example Z3, which reasons about all executions up to a given length at once. It outputs the chain of steps where a rule breaks.
Source: apalache-mc.org, the Apalache site
Where it appears · 3
- How to find a race condition in code · Specs and context
- How model checking differs from testing · Specs and context
- TLA+ vs Alloy vs Quint · Specs and context