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