The Alloy Analyzer is a tool developed by the Software Design Group
for analyzing models written in Alloy, a simple structural modeling
language based on first-order logic. The tool can generate instances
of invariants, simulate the execution of operations (even those defined
implicitly), and check user-specified properties of a model.

Alloy and its analyzer have been used primarily to explore abstract
software designs. Its use in analyzing code for conformance to a specification
and as an automatic test case generator are being investigated in ongoing
research projects.

Download the analyzer and related documentation here.