Alloy Introduction

• Readings
  • Recommended readings
• Topics covered
• Resources

Readings

• Class notes on set theory recap

• Class notes on Alloy intro

• Class notes on Alloy constraints

• Old recorded lectures
• Old class notes on an introduction to Alloy [part 1, part 2]
  • In particular try to do the exercises in these lecture notes

Recommended readings

• Alloy FAQ
• Lecture notes on first-order logic
  • by Cesare Tinelli
  • by Mario S. Alvim
• Alloy Analyzer tutorial, notes by Greg Dennis and Rob Seater [part 1, part 2]

• A hands-on introduction to Alloy, by Michael Sperberg-McQueen

• Automatic generation of security exploits with Alloy, by Caroline Trippel et al. [paper 1, paper 2]

Topics covered

• Modeling general software systems.
  • Introduction to the Alloy modeling language.
  • Alloy’s foundadions.
  • Signatures, fields, and multiplicity constrainst.
• Modeling simple domains in Alloy.
  • Generating and analyzing model instances.
• Relations and operations on them.
  • Formulas, Boolean operators and quantifiers.
  • Expressing constraints on relations using Alloy formulas.
• Functions and predicates.

Resources

• A simple family model for the Alloy Analyzer: family-1.als
• A simple family model with facts for the Alloy Analyzer: family-2.als
• A simple family model with facts and different run configurations for the Alloy Analyzer: family-3.als
• A simple family model with facts, different run configurations and assertions for the Alloy Analyzer: family-4.als