Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_13_skeleton [2007/05/02 09:57] vkuncak |
sav07_lecture_13_skeleton [2007/05/02 09:59] vkuncak |
||
---|---|---|---|
Line 17: | Line 17: | ||
* best transformer in abstract domain | * best transformer in abstract domain | ||
+ | Computation using wp. Boolean programs. Bounding cube length. | ||
+ | |||
+ | ==== Model checking ==== | ||
+ | |||
+ | Finite state space for now. | ||
+ | |||
+ | BDDs. | ||
+ | |||
+ | Bounded model checking for finite diameter systems. | ||
+ | |||
+ | ==== Counterexample-driven refinement ==== | ||
+ | |||
+ | Heuristic refinement | ||
+ | * expressions in branches | ||
+ | * adding weakest preconditions | ||
+ | * Craig's interpolation | ||