# Differences

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

 — sav07_lecture_11 [2007/04/25 18:17] (current)vkuncak created 2007/04/25 18:17 vkuncak created 2007/04/25 18:17 vkuncak created Line 1: Line 1: + ====== Lecture 11 ====== + + ===== 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 === + + [[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​PLDI03.shtml|Link to paper]] + + Section 5.4: A remark on notation: + * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,​[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$. + * 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 + + 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 === + + * [[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.