# Alloy Analyzer

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

A modeling language developed by <Daniel Jackson>. See: [Language reference](https://alloytools.org/spec.html)

https://alloytools.org

## Features

- Automatically checks every possibility based on the [small scope hypothesis](https://wiki.g15e.com/en/pages/Small%20scope%20hypothesis.txt).
- 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](https://wiki.g15e.com/en/pages/Software%20Abstractions%20-%20Logic,%20Language,%20and%20Analysis.txt)
- [Practical Alloy](https://wiki.g15e.com/en/pages/Practical%20Alloy.txt)

## Articles

- <2025-06-13> - [Alloy: Communications of the ACM](https://cacm.acm.org/research/alloy/) by <Daniel Jackson>