• English only

# Differences

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

sav07_lecture_11_skeleton [2007/04/25 15:55]
vkuncak
sav07_lecture_11_skeleton [2007/04/25 17:44] (current)
vkuncak
Line 22: Line 22:
* this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$.   * this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$.
* this is abstracted to abstract domain   * this is abstracted to abstract domain
+
+Domains used
+  * octagons (see above paper)
+  * ellipsoid
+
+Widening with tresholds.
+
+Sound approximation of real numbers with floating point calculations.
+
+Improving precision
+  * trace partitioning:​ recover some of the path sensitivity of weakest preconditions
+  * decision trees
+  * loop unrolling
+  * procedures are inlined
+
+Packing: computing relationships between groups of variables and not all variables
+  * for octagons
+  * for decision trees
+
+Results
+  * the absence of false alarms is remarkable, result of heavy tuning of the analysis to given progrma
+  * main loop invariant is 4.5MB

=== Combination of Abstractions in the ASTRÉE Static Analyzer === === Combination of Abstractions in the ASTRÉE Static Analyzer ===

+Consider Example 3 of non-monotonicity in the presence of widening. ​ The reason that the result is less precise starting from [0,0] interval for y instead of [0,9] is because widening to [0,​$+\infty$] is applied before the fixepoint interval [0,9] is reached.