progress so far
nitpick (1995)
a model finder for relational calculus
exploits inherent symmetry in type structure
painful language, didn’t scale (but caught bugs)
abstraction?
too hard to find abstractions
concrete search within finite ‘scope’
alloy/alcoa (1998)
richer language (closer to Z, UML)
SAT-based analysis scales much better
examples
architectures (COM, HLA), protocols (IPv6, phones)
code (CTAS), metamodels (UML)