The Alloy language and its analyzer have been the subject of the following talks given by faculty, students, and staff from MIT and other institutions:
Full Day Tutorial (T9), Formal Methods 2006 (FM'06)
Tuesday, August 22, 2006
McMaster University, Hamilton, Ontario, Canada
Greg Dennis & Robert Seater
Tutorial Materials
An all day interactive tutorial (6 hours over 4 sessions) introducing participants to the logic, language, and analysis of Alloy, as well as demonstrating a number of static and dynamic modeling idioms.
Mini-Tutorial, Requirements Engineering RE'05
September 1, 2005, Paris
Daniel Jackson
[PDF]
Lipari Summer
School
July 18-22, 2005
Daniel Jackson
Four lectures (all PDF colour slides):
Introduction
Language and Analysis
Idioms:
Invariants, Operations, Traces
Event
Idiom and Environmental Assumptions
(examples)
Distinguished Speakers in Software Engineering Series
Microsoft Research
March 21, 2005
Daniel Jackson
[PDF (color)]
MIT Technology Novartis IT Excellence Program @ MIT
MIT Office of Professional Education Programs
March 23, 2004
Daniel Jackson
[PDF (colour slides)]
Alloy models and visualizations from demo
Distinguished Lecture Series
University of York, England, February 2004
Daniel Jackson
[PDF (colour slides)]
Alloy models and visualizations from demo
An overview of Alloy and its applications, with an emphasis on the
key ideas behind the research program.
Keynote, 3rd International Conference of B and Z Users
(ZB2003)
Turku, Finland, 4 June 2003
Daniel Jackson
[PDF (colour slides)]
Alloy models and visualizations from demo
A tour of Alloy, with an emphasis on the difference between Alloy
and Z.
Praxis Critical Systems, Bath, UK
April 25, 2003
Daniel Jackson
[PDF (colour slides, for printing)]
[PDF (colour slides, animated)]
Alloy models and visualization
A whirlwind tour of Alloy for an audience familiar with formal methods such as Z. In one small example illustrates basic semantics, simulation and checking, operation- and trace-based analyses.
Marktoberdorf Summer School
Germany, July 2002
Daniel Jackson
Introduction [PDF,
animated] [PDF,
for printing]
Logic [PDF,
animated] [PDF,
for printing]
Language [PDF,
animated] [PDF,
for printing]
Analysis [PDF,
animated] [PDF,
for printing]
Bakery [PDF,
animated] [PDF,
for printing]
Elevator [PDF,
animated] [PDF,
for printing]
A series of four and a half lectures on Alloy, aimed at students with an interest in a mathematical approach to modelling. No background required beyond elementary logic. The elevator case study was replaced by the bakery example at the last minute (since it had been discussed by John Rushby in his lectures). In that example, the modelling of a procss in the critical section as holding no ticket is bogus and has to be fixed (but the general structure of the model, and the trace-based analysis still holds).
[PDF (colour slides)]
Alloy
models and visualization
Daniel Jackson
Distinguished Lecture Series
Michigan State University, November 2001.
Overview of the Alloy approach to modelling for a general computer science audience.
[PDF (colour slides)]
Alloy
models and visualization files
Daniel Jackson (joint work with Mandana Vaziri and Allison
Waingold)
Workshop on New Directions in Software Technology
St. John, US Virgin Islands, December 2001
Preliminary work. Shows how to construct a simple logical model of Java views. Illustrated on a procedure that manipulates iterators and lists.
[PDF (colour slides)]
Alloy model
Daniel Jackson, Ilya Shlyakhter, Manu Sridharan
ACM SIGSOFT Conf. Foundations of Software Engineering/European
Software Engineering Conference (FSE/ESEC '01)
Vienna, September 2001.
Describes new version of Alloy, focusing on the fundamental idea of the signature. Illustrated on a small railway example. The paper contains many details not covered, including polymorphism, signature extension and a demonstration of the use of the mechanism in a variety of idioms.
NASA Ames, August 14, 2001
Daniel Jackson, MIT
[PDF (colour slides)],
[PDF (black on white, two/page)]
Overview of Alloy approach to the use of models in software development. Illustrates application of Alloy at both abstract design and code design levels to a text tagging program.
Keynote Lecture
Formal Methods Europe
Berlin, March 14, 2001
Daniel Jackson, MIT
[downloads]
[PDF]
Formal methods have offered great benefits, but often at a heavy price. For everyday software development, in which the pressures of the market don't allow full-scale formal methods to be applied, a more lightweight approach is called for. I'll outline an approach that is designed to provide immediate benefit at relatively low cost. Its elements are a small and succinct modelling language, and a fully automatic analysis scheme that can perform simulations and find errors. I'll describe some recent case studies using this approach, involving naming schemes, architectural styles, and protocols for networks with changing topologies. I'll make some controversial claims about this approach and its relationship to UML and traditional formal specification approaches, and I'll barbeque some sacred cows, such as the belief that executability compromises abstraction.
Includes sneak preview of new version of Alloy, with structuring mechanism and arbitrary-arity relations.
Daniel Jackson, MIT
IFIP Working Group 2.9 on Requirements Engineering
Hawk's Cay, Florida
February 19, 2001
[downloads]
[PDF]
A new version of Alloy with structuring. BART example revisited. Why declarative style is important.
Invited Lecture
7th International Static Analysis Symposium
Santa Barbara, CA, June 29, 2000
Daniel Jackson, MIT
[downloads]
Overview of Alloy and its analyzer, with sample applications to models and code.
Lab for Computer Science Annual Retreat
MIT, June 26, 2000
Daniel Jackson, MIT
[downloads]
A brief talk describing Sarfraz Khurshid's case study of Intentional Naming using Alloy.
Future of Software Engineering Track
International Conference on Software Engineering
Limerick, Ireland
May 2000
Daniel Jackson, MIT
[downloads]
Based on a paper with Martin Rinard.
IFIP Working Group 2.3 on Programming Methodology
Newcastle, England, April 4, 2000
Daniel Jackson, MIT
[Part A] /
[Part B]
Part A gives an outline of the Alloy modelling language and shows how it was used in an analysis of Microsoft COM (joint work with Kevin Sullivan). Part B describes the analysis of Alloy by translation to SAT, and includes brief comments on a new symmetry breaking scheme developed by Ilya Shlyakhter.
Workshop on Model Checking & Program Analysis
Schloss Ringberg, February 21, 2000
Daniel Jackson, MIT
Joint work with Mandana Vaziri
[downloads]
I presented a new method for finding bugs in code using SAT. The code of a procedure is translated into an Alloy formula. A second formula is obtained by combining this formula with a user-defined specification, whose models are executions of the procedure that violate the spec. The Alcoa checker is then used to find models. I illustrated the use of this method to find shape analysis bugs in a benchmark suite of programs used previously by Sagiv et al. The method is not sound, since it may miss bugs, but is complete (so long as datatypes aren't abstracted). The merit of the approach is its ability to handle user-defined specs, not only to check code against, but also as surrogates for called procedures.
IFIP WG 2.9
Flims, Switzerland, February 7, 2000
Daniel Jackson, MIT
[downloads]
I explained the motivation behind lightweight formal methods, and presented Alloy, a new lightweight object modelling language. I illustrated the simplicity of aspect by showing how it treats partial functions. I showed how to use Alloy and its automatic analyzer Alcoa to investigate the placement of gates in the BART system, and to check that a gate policy has the intended safety consequences. Finally, I explained why the problem of analyzing Alloy models is hard -- often involving the consideration of 10^100 states -- but in practice usually possible in seconds.
ICSE Tutorial - International Conference on Software
Engineering
Tuesday 25th May 2004, Scotland
Jin Song
Dong, National University of Singapore
[downloads]
Schloss Dagstuhl Workshop "Reasoning about shape"
Dagstuhl, Germany, March 3-7 2003
Michael Huth, Imperial College London
[PS]
Distributed Software Engineering Seminar
Imperial College London, February 7 2003
Michael Huth, Imperial College London
[PS]
Lecture 12 of CS294: Topics in Software Engineering
University of California, Berkeley, October 4 2001
Alex Aiken,
University of California, Berkeley
[PDF]