Alloy is a declarative language for lightweight modeling and analysis of software. The core of the language is based on first-order relational logic, which offers an attractive balance between analyzability and expressiveness. The logic is expressive enough to capture the intricacies of real systems, yet it 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.

 

The article provides an overview of Alloy in the context of its three largest application domains (lightweight modeling, 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 analyzer based on SMT).