alloy

Citations

Official Homepage

github

Alloy is a language for describing structures and a tool for exploring them. It can check properties of the model by generating counterexamples. We can automatically verify an assert statement up to a specified (finite) depth. If the statement does not hold, Alloy produces a counterexample. Alloy is sound and complete up to the specified depth.

Alloy is best suited for describing and reasoning about a set of structures, such as all the possible security configurations of a web application, or all the possible topologies of a switching network.

Behind the scenes, Alloy is based on a theory of atoms and relations. However, set-theoretic reading of models usually suffices.

Alloy is a product of the Software Design Group at MIT.

Tutorial for Alloy Analyzer 4.0 is a short and good starting point.