analyzing code
idea
treat procedure as operation to check with Alcoa
compose from declarative specs of statements
combine paths with disjunction
features
expressive property language
no need to adapt analysis to properties
counterexample is trace of states
modular – use spec in place of code
unsound – small scope, few unrollings