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:57]
vkuncak
@@ Line 1: / Line 1: @@
-====== Predicate abstraction ======
+====== Predicate abstraction techniques ======
+See [[predicate abstraction]] papers.
+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
-[[Predicate abstraction]]