The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.
*Newsflash* Alloy Analyzer 4.1.2 is now available for testing!
| Alloy Analyzer 4.1.2 | - | downloads, quickstart guide |
| Alloy Analyzer 3.0 | - | downloads, analyzer, reference manual, troubleshooting |
| New in v3.0 | - | how Alloy 3.0 differs from Alloy 2.0 |
| Quick Start | - | brief overview of using Alloy to analyze models |
| Online Tutorial | - |
introduction to Alloy and advice on writing models
offline versions: (index) (PDF zip) (HTML zip) |
| FAQ | - | frequently asked questions, Alloy's history and philosophy |
| Publications | - | papers and theses on Alloy |
| Alloy Workshop '06 | - | programme and papers from workshop held in Nov 06 |
| Case Studies | - | case studies using Alloy |
| Talks | - | talks about Alloy |
| Courses | - | Alloy as a teaching tool |
| Alloy-Discuss | - | Yahoo discussion group |
To receive emails about Alloy updates and releases, add yourself to the alloy announce email list.
Please send suggestions and bug reports to 
.
Please send general questions and comments to the alloy-discuss yahoo group.
© 2000-2006 Software Design Group
Research conducted by the Software Design Group described on this website was funded, in part, by grant 0086154 from the ITR program of the National Science Foundation, and by the High Dependability Computing Program from NASA Ames cooperative agreement NCC-2-1298.