Paper: PDF (282.4 KB).

     The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization, the symbolic manipulation of expressions to improve the precision of abstract transfer functions, the octagon, ellipsoid, and decision tree abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds, delayed) and the automatic determination of the parameters (parametrized packing).

\bibitem{BlanchetEtAl-PLDI03}
B{.} Blanchet, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
   Min\'e, D{.} Monniaux, and X{.} Rival.  
\newblock A Static Analyzer for Large Safety-Critical Software.
\newblock \emph{Proc{.} ACM SIGPLAN 2003 Conference on Programming Language
   Design and Implementation} (PLDI'03), San Diego, California , USA, June
   7--14, 2003, pp{.} 196--207.  ACM Press, 2003.

@InProceedings{BlanchetEtAl-PLDI03,
   author =    {B{.} Blanchet and P{.} Cousot and  R{.} Cousot and J{.} Feret and
                L{.} Mauborgne and A{.} Min\'e and D{.} Monniaux and X{.} Rival},
   title =     {A Static Analyzer for Large Safety-Critical Software},
   pages =     {196--207},
   booktitle = {Proceedings of the ACM SIGPLAN 2003 Conference on Programming
                Language Design and Implementation (PLDI'03)},
   address =   {San Diego, California, USA},
   publisher = {ACM Press},
   month =     {June 7--14},
   year =      2003,
}