• 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 Both sides previous revision Previous revision 2007/04/25 17:44 vkuncak 2007/04/25 15:55 vkuncak 2007/04/25 11:04 vkuncak 2007/04/25 08:54 vkuncak created 2007/04/25 17:44 vkuncak 2007/04/25 15:55 vkuncak 2007/04/25 11:04 vkuncak 2007/04/25 08:54 vkuncak created 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 === * [[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​ASIAN06.shtml|Link to paper]] * [[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.