RESOURCE
tools
Because it offers a powerful analysis engine for a very general logic, Alloy and its model finding engine Kodkod have been used as backends for many more specialized tools.
Alloy Citations
| Google scholar | A sample of over 1200 papers discussing Alloy |
| case studies | Selected papers describing applications of Alloy |
| translations | Papers on translating a dozen other languages into Alloy |
| theses | Theses about Alloy |
select tools built on alloy and kodkod
| Alloy* | A general-purpose, higher-order, relational constraint solver |
| aRby | An embedding of Alloy in Ruby |
| 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. |
| Lightning | An Eclipse plugin allowing to specify graphical DSLs in Alloy |
| Echo | A tool for model repair and transformation built over Alloy |