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.

Colour slides for printing:
http://people.csail.mit.edu/dnj/talks/praxis/praxis.noanim.pdf

Colour slides, animiated:
http://people.csail.mit.edu/dnj/talks/praxis/praxis.anim.pdf

Alloy models and visualization:
http://people.csail.mit.edu/dnj/talks/praxis/models