Masterclasses
GOTO Chicago 2019

Thursday May 2
09:00 –
16:00
Location: 202

Getting it Right the First Time: An Introduction to Alloy Modeling

Most software flaws come from one of two places. When the code doesn’t match our expectations, it could be that the code is wrong. Most software correctness techniques - types, tests, etc - are used to check the code. But it could instead be that the code is correct and our expectations are wrong: there’s a fundamental error in our design. These errors, called specification errors, are some of the most subtle and dangerous bugs. They can span multiple independent programs, occur in convoluted race conditions, or depend on physical phenomena. Our regular tools simply can’t find them.

Instead, we can find them by designing better. By writing your blueprint in a specification language, you can directly test your conception of the system. Automatic tools, such as model checkers and SAT solvers, then explore the entire design space to see if it actually has the properties you want. And since it works on the design itself, we can fix issues before we’ve written a single line of code.

In this workshop, attendees will learn how the basics of one such specification language, called Alloy, and how to apply it to real-world business problems. We will cover everything from data modeling to microservice architectures. By the end of this class attendees should be able to write their own basic specs and use them to identify issues in their software designs.

Who should attend this masterclass: People interested in testing, design, or formal methods

Academic level: Intermediate / Advanced

What is the take away from this masterclass: Attendees will learn how to use Alloy, how to do formal specification, and how to find issues with systems before making them.

Hillel Wayne
Author of Practical TLA+, expert in applying formal methods to real-world problems
Organized by