P. Cousot, Formalizations of Abstraction in the Abstract Interpretation Theory

Patrick Cousot.
Formalizations of Abstraction in the Abstract Interpretation Theory.
« The Challenge of Software Verification », Dagstuhl Seminar 6281, Schloss Dagstuhl, Wadern, Germany, July 9—13, 2006.
Abstract:
   We discuss the formalizations of the abstraction of a property/collecting semantics in abstract interpretation theory using Galois connections when each concrete property has a best abstract approximation and otherwise an abstraction function or a concretization function, which in practice is prefered because it delays the choice of the approximation of concrete properties by (if possible minimal) abstract properties until the context of this abstraction is known.
   To ensure convergence of the abstract iterates when computing the abstract semantics, we recall that the widening/narrowing approach can always be made more precise than any further abstraction satisfying the ascending chain condition, a fortiori than any finite one.
   It is necessary to design complex abstraction by parts using systematic mthods to combine the parts, such as the reduced product. The iteraction with widenings is discussed.
   These design principles have been applied in the ASTRÉE Static Analyzer for proving the absence of runtime errors in safety critical real-time synchronous control/command software. A demonstration of the ASTRÉE Static Analyzer shows a few key points in its design. ASTRÉE Static Analyzer has shown to be able to find design errors in programs of hundreds of thousands of lines in hours, even errors than can never show up in the context in which the program is operated thus showing the advantage of static analysis over testing or runtime checking.
Keywords:
Abstract Interpretation, Galois Connection, Abstraction, Concretization, Widening, Reduced Product, Static Analysis, Embedded Safety Critical Control/Command Software, Runtime Errors.
Slides of the 15 mn presentation: .pdf.

Typescript (.pdf) of the 15 mn demonstration of the ASTRÉE Static Analyzer, C programs used for the demonstration and the screen snapshot (.tiff, .pdf) of the ASTRÉE user interface.

Bibliographic reference:

\bibitem{Cousot-DagstuhlSeminar6281}
P.~Cousot.
\newblock Formalizations of Abstraction in the Abstract Interpretation Theory.
\newblock \emph{The Challenge of Software Verification}, 
         Dagstuhl Seminar 6281, Schlo\ss\ Dagstuhl, Wadern, Germany, July 9--13, 2006.

@conference{Cousot-DagstuhlSeminar6281,
   author =    {P{.} Cousot},
   title =     {Formalizations of Abstraction in the Abstract Interpretation Theory},
   note    =   {\emph{The Challenge of Software Verification}, 
                Dagstuhl Seminar 6281, Schlo\ss{}\ Dagstuhl, Wadern, Germany},
   month =     {July 9--13},
   year =      2006,
}

copyright notice
Last modified: Monday, 07-May-2012 17:51:03 EDT