applications
Alloy is used in a wide variety of applications. The page provides links to some tools built on Alloy and Kodkod (Alloy’s model finding engine), and to lists of citations from Google Scholar of papers that discuss applications of Alloy.
Alloy Citations
- citations
- A sample of over 600 papers discussing Alloy
- case studies
- A hundred papers describing applications of Alloy
- translations
- Papers on translating a dozen other languages into Alloy
Select Tools Built on Alloy and Kodkod
- Forge
- A bounded verifier for Java code
- Squander
- Unified execution of imperative and declarative code
- Alloy4Eclipse
- Eclipse plugin for Alloy 4
- DynAlloy
- An extension of Alloy with procedural actions
- TACO
- A bounded verifier for Java annotated with JML
- Equals Checker
- A tool for checking equals methods in Java
- Nitpick
- A counterexample generator for Isabelle/HOL
- Margrave
- A security policy analyzer for firewalls
- Secrecy Modeling Language (SML)
- A language for composing and validating security models.