swMATH ID: 1247
Software Authors: Jackson, Daniel
Description: Alloy: A new technology for software modelling. Alloy is a lightweight language for software modelling. It’s designed to be flexible and expressive, and yet amenable to fully automatic simulation and checking. At its core, Alloy is a simple first order logic extended with relational operators. A simple structuring mechanism allows Alloy to be used in a variety of idioms, and supports incremental construction of models. Alloy is analyzed by translation to SAT. The current version of the tool uses the Chaff and Berkmin solvers; these are powerful enough to handle a search space of 2 100 or more. Alloy has been applied to problems from very different domains, from checking the conventions of Microsoft COM to debugging the design of a name server. Most recently, we have used it to check distributed algorithms that are designed for arbitrary topologies. We are also investigating the use of Alloy to analyze object-oriented code.
Homepage: http://alloy.mit.edu/alloy/
Related Software: Alcoa; SPIN; Z; Mace4; Z/EVES; Chaff; Kodkod; PVS; Isabelle/HOL; Coq; TestEra; Circus; FDR2; NuSMV; z3; ProB; Prover9; Why3; TPTP; RelView
Cited in: 23 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Alloy: A new technology for software modelling. Zbl 1043.68520
Jackson, Daniel

Citations by Year