LARA

Differences

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

Link to this comparison view

sav07_lecture_13 [2007/05/02 15:20] (current)
vkuncak created
Line 1: Line 1:
 +====== Predicate abstraction techniques (first part) ======
 +
 +See [[predicate abstraction]] papers.
 +
 +Three aspects:
 +  * abstraction
 +  * model checking (finite state or pushdown system)
 +  * counterexample-driven refinement
 +
 +Today: abstraction
 +
 +==== Abstraction ====
 +
 +Main readings:
 +  * [[http://​www-verimag.imag.fr/​~graf/​biblio.php?​view=full#​GrafSaidi97|Construction of abstract state graphs with PVS]]
 +  * [[http://​www.mpi-sb.mpg.de/​~podelski/​papers/​cartesian.ps|Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format)]]
 +  * [[http://​doi.acm.org/​10.1145/​378795.378846|Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213]]
 +
 +
 +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
 +
 +Examples.
 +
 +Computation using wp.  Weakest predicate abstraction of a given formula. ​ 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
 +Approximations:​
 +  * bounding cube length to 3
 +  * distributing approximation through logical operations
 +