RESOURCE
courses
Alloy is an ideal tool for teaching software modeling, since it offers a simple relational modeling language and an accessible standalone tool that provides novices with instant feedback.
It has been widely used in undergraduate and graduate courses on software analysis modeling and design; on model checking, verification and logic; on discrete math; and on computer systems.
courses using alloy
| Logic for Systems. | Dr. Tim Nelson, Brown University, Spring 2014., 2015., 2016. |
| Enterprise and service-oriented architecture. | Wegmann Alain, EPFL, Spring 2014., 2015., 2016. |
| Métodos Formais em Engenharia de Software: Análise e Teste de Software. | Prof. Manuel Alcino Cunha, University of Minho, Portugal, 2014., 2015. |
| Métodos Formais em Engenharia de Software: Especificação e Modelação. | Prof. Jose Nuno Oliviera, University of Minho, Portugal, 2014., 2015. |
| CSI5118 (COMP 5302) Automated Verification And Validation Of Software. | Dr. Stéphane S. Somé, University of Ottawa, Winter 2015. |
| Formal Methods in Software Development. | Prof. Laura Dillon, Michigan State University, Fall 2014. |
| SWEN 220: Mathematical Models of Software. | Prof. Tom Reichlmayr, Rochester Institute of Technology, Fall 2014. |
| CS:5810 Formal Methods in Software Engineering. | Prof. Cesare Tinelli, University of Iowa, Fall 2014. |
| E0 272 Formal Methods in Software Engineering. | Deepak D’Souza and K. V. Raghavan, Indian Institute of Science, Bangalore, Spring 2014. |
| CS517 Software Specification & Design. | Prof. Robert B. France, Colorado State, Spring 2014 |
| CS 290C - Formal Models for Web Software. | Prof. Tevfik Bultan, UC Santa Barbara, Spring 2013. |
| Rigorous Software Development. | Prof. Thomas Wies, New York University, Spring 2013. |
| Formal Methods in Networking. | Dr. Sanjai Narain, Princeton University, Spring 2010. |
| Automatic Program Checking. | Prof. Mana Taghdiri, Karlsruhe Institute of Technology, Spring 2010. |
| CIS 771 Software Specifications. | Prof. Robby, Kansas State University, Online course. |
alloy-related tools for teaching
| 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 |