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 10:20]
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.
+Precision-preserving optimizations:
+  * cubes in increasing order
+  * do not update variables if command cannot change them
+  * cone of influence to reduce the number of predicates to consider
+  * syntactic construction of predicates
+  * caching of calls to theorem prover
+Further approximations:
+  * bounding cube length to 3
+  * distributing approximation through logical operations
+==== Model checking ====
+Finite state space for now.
+Bounded model checking for finite diameter systems.
+BDDs: http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf
+==== Counterexample-driven refinement ====
+Heuristic refinement
+  * expressions in branches
+  * adding weakest preconditions
+  * Craig's interpolation