Tuesday, February 12, Volen 101, 2:00-3.00 pm
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 satisfiability: this means that as the SAT community improves its technology, the Alloy analyzer scales better.
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.
Host: Liuba Shrira