Alloy at BU

The term Alloy refers to both a formal language and an automated analyzer. The Alloy Analyzer translates the user models into SATs, i.e., boolean satisfiability problems. The Alloy language is a declarative specification language for modeling complex structures and behaviors in a (distributed) system. Alloy is based on first order logic, and is designed for model enumeration (also known as model checking). The Alloy language is simple, expressive, and is based on the notions of relations and sets (for more information go to [Alloy at MIT]).

Publications

Saber Mirzaei and Flavio Esposito.
An Alloy Verification Model for Consensus-Based Auction Protocols
Accepted to ADSN 2015, April 2015. [PDF][PS]
Saber Mirzaei, Sanaz Bahargam, Richard Skowyra, Assaf Kfoury and Azer Bestavros.
Using Alloy to Formally Model and Reason About an OpenFlow Network Switch
BUCS Technical Report Archives, July, 2013. [PDF][PS]
Mark C. Reynolds.
Modeling the java bytecode verifier
Published in Science of Computer Programming, March, 2013. [PDF][PS]
Mark C. Reynolds.
Lightweight modeling of java virtual machine security constraints
ABZ 2010. [PDF][PS]

Implemented Models

The Alloy model of Consensus-Based Auction Protocol can be downloaded from [this] github repository.

People