PV3 Alloy Analyzerchecks user-specified assertions in Alloy models

Application domain/field

State machines with complex structured state

Type of tool

Constraint solver

Expected input

Model (with assertions/properties)


Alloy language

Expected output

Counterexample or "assertion may be valid"


The Alloy Analyzer translates the given problem into a boolean formula which is then handed to a SAT solver. When the SAT solver is done, the solution is translated back into the language of the original model. The user needs to specify a scope that bounds the size of the domains thereby making the problem finite and thus reducible to a boolean formula. Uses SAT solvers to refute a formula. It uses Sat4j, MiniSat, plingeling and Glucose for SAT solving.


Domains (in the model) are bound by the user, resulting in a finite problem.


ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.