related work
shape analysis
k-limiting
loss of completeness, not soundness
Sagiv, Reps, Wilhelm
relational state
‘execute’ with transfer functions
instrumentation for precision
pre-post relationships?
model checking
Kautz, McAllester & Selman: reachability with SAT
Biere, Cimatti, Clarke, Fujita & Zhu: bounded LTL
theorem proving
ESC : sound but less expressive properties