1) Every branch gets a goal for each direction. 2) Need single definition point...SSA like semantics Model checking is complete when For each branch it is either 1) Each exit is covered 2) The incoming function is covered 3) A function is covered if A) all addresses of all stores are resolved and either B) all inputs to function are covered and C) each combination of inputs to a function are either i) covered or ii) unschedulable 4) A read is covered if for each value stored by a store that can access the same address it: a) has seen all values b) the store can't store the value to same address c) it isn't schedulable...