alcoa: alloy constraint analyzer
how Alcoa is used
start with minimal description
consistent? (too many constraints?)
consequences? (too few?)
what analysis involves
finding models of relational formula
for op, sample transition
for negation of assertion, counter
scope
limit #elements in basic types
in scope of 3, 2^9 values / relation
FSE 96 (BDDs) FSE 98 (WalkSAT) 1999 (SATO)