Differences

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

--- sav07_lecture_11_skeleton [2007/04/25 08:54]
vkuncak created
+++ sav07_lecture_11_skeleton [2007/04/25 17:44]
vkuncak
@@ Line 1: / Line 1: @@
+===== Modular analysis of procedures =====
+Inlining specifications.  Last part of [[SAV07 Homework 4]].
+Postconditions that refer to values of variables in the precondition.
+The meaning of modifies clauses.
 ===== ASTREE Static Analyzer =====
+=== The Octagon Abstract Domain ===
+[[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|Link to paper]]
 === A Static Analyzer for Large Safety-Critical Software ===
@@ Line 10: / Line 23: @@
   * this is abstracted to abstract domain
-=== The Octagon Abstract Domain ===
+Domains used
+  * octagons (see above paper)
+  * ellipsoid
-[[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|Link to paper]]
+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 ===
   * [[http://www.di.ens.fr/~cousot/COUSOTpapers/ASIAN06.shtml|Link to paper]]
+Note Section 4.1 on how many of the standard assumptions of the domain do not hold any more for such a complex 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.
+Section 5 deals with communicating information between different domains.  The functions that are defined are mostly various form of approximating conjunction (intersection of sets of states).  There are many such functions because arguments and results can belong to different domains.