automatically discover useful facts about programs dynamic tools can only infer likely invariants abstract state <- collections of concrete states
static alanysis sacrifices completeness?! but soundness is ok
iterative approximation
sound - all claims are true (no false positives) complete- if there is anything to claim, it will be claimed (no false negatives)
reachability is undecidable
no sound and complete
data flow analysis
flow sensitivity
flow sensitivity via SSA
flow vs path sensitivity