Alloy Analyzer

A modeling language developed by Daniel Jackson. See: Language reference

alloytools.org

Features

• Automatically checks every possibility based on the small scope hypothesis.
• Treats everything as an n-ary relation. Examples: [{x}], vectors as [{x, y}], and matrices as [{w, x}, {y, z}].
• Uses a SAT solver internally.

Publications

• Software Abstractions: Logic, Language, and Analysis
• Practical Alloy

Articles

• 2025-06-13 - Alloy: Communications of the ACM by Daniel Jackson