Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_13_skeleton [2007/05/02 09:52]
vkuncak created
+++ sav07_lecture_13_skeleton [2007/05/02 09:59]
vkuncak
@@ Line 1: / Line 1: @@
-====== Predicate abstraction ======
+====== Predicate abstraction techniques ======
+See [[predicate abstraction]] papers.
-[[Predicate abstraction]]
+Three aspects:
+  * abstraction
+  * model checking (finite state or pushdown system)
+  * counterexample-driven refinement
+==== Abstraction ====
+Design space of abstractions:
+  * Cartesian product of abstractions for each predicate
+  * powerset with cartesian abstraction (ignores dependences in pre and post)
+  * powerset that takes into account the entire state (reduced product)
+  * focus (splitting, case analysis)
+  * 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