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