notes

   1 1) Every branch gets a goal for each direction.
   2 2) Need single definition point...SSA like semantics
   3
   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
  10          and either
  11    B) all inputs to function are covered and
  12
  13    C) each combination of inputs to a function are either
  14       i) covered or
  15       ii) unschedulable
  16
  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...