Lab for Automated Reasoning and Analysis LARA


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

Link to this comparison view

sav07_lecture_13_skeleton [2007/05/02 15:18]
sav07_lecture_13_skeleton [2007/05/02 15:19] (current)
Line 25: Line 25:
   * best transformer in abstract domain   * best transformer in abstract domain
-Computation using wp.  Boolean programs.+Examples. 
 +Computation using wp.  Weakest predicate abstraction of a given formula.  Boolean programs.
 Precision-preserving optimizations:​ Precision-preserving optimizations:​
Line 33: Line 35:
   * syntactic construction of predicates   * syntactic construction of predicates
   * caching of calls to theorem prover   * caching of calls to theorem prover
-Further approximations:+Approximations:
   * bounding cube length to 3   * bounding cube length to 3
   * distributing approximation through logical operations   * distributing approximation through logical operations
sav07_lecture_13_skeleton.txt · Last modified: 2007/05/02 15:19 by vkuncak
© EPFL 2018 - Legal notice