Z3
Formal verification · an SMT solver from Microsoft Research
created · updated
The best-known SMT solver: a program that picks values for given conditions. For example, for “x plus y equals ten, x minus y equals two” it answers “x is six, y is four”, or proves that no solution exists. Apalache gives Z3 the conditions obtained from a model and builds the chain of steps to the rule violation from its answer.
Source: Z3, the GitHub repository
Where it appears · 1
- How model checking differs from testing · Specs and context