P. Cousot, Advances and Challenges in Static Program Analysis by Abstract Interpretation

Patrick Cousot.
Advances and Challenges in Static Program Analysis by Abstract Interpretation.
Colloquia Patavina, Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Padova, Italy. Tuesday February 19^th, 2008.
Abstract:
     The correctness proof objective of formal methods is to show that a semantic model of the possible computations of a program satisfy a formal specification. Formal methods must confront various problems, including the definition of the semantics of programming and specification languages as well as the automation of undecidable proofs.
     Abstract interpretation introduces the ideas of abstraction and approximation in formal methods which is mandatory to cope with complex software systems and undecidability. It formalizes the idea that sound reasonings on abstract models of program semantics should be valid on any concrete computation. It also provides completeness conditions for correctness proofs to succeed in the abstraction. Abstract interpretation can be applied to the design of programming languages semantics, deductive methods, abstract model-checking, typing, static analysis, program transformation, and many other applications at various levels of abstraction.
     Static analysis consists in proving that an abstraction of a program semantics( overapproximating all program computations) implies an implicit safety or security specification. The abstraction must be chosen to be sound, precise enough to imply the specification, and approximate enough to be cheaply representable and computable . By undecidability, this approximation introduces spurious behaviors which can be at the origin of false alarms that is fictive violations of the specification.
     The experience of ASTRÉE (www.astree.ens.fr), shows that static analyzer to prove the absence of runtime errors in safety critical synchronous real-time control/command software can be both sound, efficient and precise when applied to domain-specific family of programs. The challenge is to broaden the considered class of programs and properties.
Slides of the 55 mn presentation:.pdf .

Bibliographic reference:

\bibitem{Cousot-Padova-2008-02-19}
P.~Cousot.
\newblock Advances and Challenges in Static Program Analysis by Abstract 
          Interpretation.
\newblock \emph{Colloquia Patavina}, Dipartimento di Matematica Pura ed 
          Applicata, Universit{`a} degli Studi di Padova, Padova, Italy, 
          February 19${^\mathrm{th}}$ 2008.

@inProceedings{Cousot-Padova-2008-02-19,
   author =    {P{.} Cousot},
   title =     {Advances and Challenges in Static Program Analysis by Abstract 
                Interpretation},
   booktitle = {Colloquia Patavina},
   address =   {Dipartimento di Matematica Pura ed Applicata, Universit{`a} degli Studi di Padova, Padova, Italy},
   month =     {February 19${^\mathrm{th}}$ 2008},
   year =      2008,
}

copyright notice
Last modified: Monday, 07-May-2012 18:47:15 EDT