Alloy is a declarative language for lightweight modelling and analysis of software.
The core of the language is based on first-order relational logic, which offers an
attractive balance between analysability and expressiveness. The logic is
expressive enough to capture the intricacies of real systems, but is also simple
enough to support fully automated analysis with the Alloy Analyzer. The Analyzer is
built on a SAT-based constraint solver and provides automated simulation, checking
and debugging of Alloy specifications. Because of its automated analysis and
expressive logic, Alloy has been applied in a wide variety of domains. These
applications have motivated a number of extensions both to the Alloy language and
to its SAT-based analysis. This paper provides an overview of Alloy in the context
of its three largest application domains, lightweight modelling, bounded code
verification and test-case generation, and three recent application-driven
extensions, an imperative extension to the language, a compiler to executable code
and a proof-capable analyser based on SMT.