A Decade of Alloy: Ideas, Applications, and New Directions

Alloy is a modeling language that combines ideas from relational algebra, object-oriented programming languages and specification formalisms. It's now been in use for a decade, and has been applied in many different settings: not just design analysis, for which it was conceived, but also test case generation, program verification, website synthesis, and more. This talk is three-in-one. First, I'll give a whirlwind tour of the essential ideas of Alloy: its nifty generalization of relational join, its strange but largely invisible type system, its reduction of analysis and simulation to SAT solving, and its support for unusual idioms. Second, I'll describe some of its successful applications, and the sometimes embarrassing mistakes its analysis has uncovered. Third, I'll tell you about some of the new directions our research is taking, and what I see for the future of modeling and analysis.

Additional CS events.