shape analysis with SAT Daniel Jackson & Mandana Vaziri Software Design Group, MIT LCS Schloss Ringberg · February 21, 2000
why software model checking?
how would model checking differ for software?
progress so far
BART railway problem
sample alloy model
alcoa: alloy constraint analyzer
analyzing code
example
programming language
formula language
modelling state
sequential composition
translation scheme
translation rules
from formula to counterexample
null derefs (1)
null derefs (2)
example in full
jumps
a small experiment
sample specs
what next?
related work
conclusion
Email: dnj@lcs.mit.edu
Home Page: http://sdg.lcs.mit.edu/~dnj
Download presentation source