Alloy Modelling
Lightweight formal methods refer to the art of tinkering with compact and precise descriptions (i.e., models) of software systems in order to understand salient design details and to find design flaws. The Alloy Analyzer, developed by MIT's Software Design Group, is a tool that can simulate executions, check user-specified properties, and instantiate invariants of models described in Alloy -- a modelling language based on first-order logic.
As part of the Alloy development team, I developed a module importing subsystem that allows users to parameterize and reuse common models. I also implemented a feature known as "unsat core visualization," which helps users to visualize bugs in their models by highlighting parts of the specification that may have been overconstrained.
I have also conducted a few case studies of software protocols using Alloy:
- Case Study in Alloy Modelling: A Common Profile for Presence [pdf report w/ model]
- Case Study in Transaction Locking [html report] [model]