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