Eunsuk Kang, Software Design Group at MIT, USA

Alloy is a modeling language designed for specifying and analyzing software systems. Its underlying toolkit, the Alloy Analyzer, provides fast, automatic analysis that can be used to check a system model against an assertion, detect inconsistencies in a specification, or generate simulation traces. In the past, the tool has been used to model and analyze a variety of systems, including a flash file system, software for smart cards, network and web protocols, a Java virtual machine, Apache server configuration, and social network privacy, among others.

In this talk, I will present an introduction to Alloy, and demonstrate some of its applications. In particular, I will show how the tool can be used to specify and reason about properties of safety critical systems during a development process.

More information about the tool can be found in [1].

[1] http://alloy.mit.edu