Daniel Jackson’s book Software Abstractions offers a gentle and detailed introduction to modeling and analysis in Alloy through a sequence of short examples.

Alloy is an ideal tool for teaching software modeling, since it offers a simple relational modeling language and an accessible standalone tool that provides novices with instant feedback.

FAQ about the Alloy language and tools; reference guides; tutorials and quick introductions; …

A collection of Alloy models to peruse…

Alloy has been used as a design and analysis tool in a wide variety of applications and projects in industry, research and teaching.

Because it offers a powerful analysis engine for a very general logic, Alloy and its model finding engine Kodkod have been used as backends for many more specialized tools.