daniel jacksonstatic analysis symposium ·santa barbara · june 2k
my green eggs and ham
plan of talk
an example
kernel: type decls
kernel: expressions
kernel: formulas
shorthands
more shorthands
sample model: intentional naming
intentional naming
tree representation
strategy
alloy model: state
alloy model: constraints
checking assertions
results
counterexample
time & effort
other modelling experiences
why modelling improves designs
how analyzer works
architecture
example
translation scheme
translation
tricks
how (not) to delete
specifying delete
hacking delete (1)
hacking delete (2)
step 1: unroll control flow graph
step 2: encode control flow
step 3: encode dataflow
frame conditions
sample results
promising?
summary
related work
PPT Slide