P. Cousot, Parameterized Refinement in Abstract-Interpretation-Based Static Analysis Veri

Patrick Cousot.
Parameterized Refinement in Abstract-Interpretation-Based Static Analysis.
Verication group, Computer Science, NYU, New York, NY, USA, April 20^th 2008.

Abstract:
We discuss the design of abstract-interpretation-based static analyzers for the verification of domain specific specifications and programs with the objectives of both soundness and zero false alarm (such as e.g. ASTRÉE). It is explained that the abstract domain must include the specification domain as well as the weakest inductive invariants for all the programs in the family. It follows that the design of the adequate abstraction is extremely difficult and must be done empirically by trial and failure (through false alarms). There exists a semi-algorithm for the task but beyond non-termination the main problems are the unnecessary case-based overprecision and extreme inefficiency of the refined domain. The challenge is therefore to design abstraction that are precise enough to avoid false alarms, coarse enough to allow for scalability and for which good computer representations and efficient algorithms can be designed and implemented. The weak reduced product can be built-in in the static analyzer to easily incorporate such manually refined abstract domains. The approach is illustrated by an overview of the design of ASTRÉE.
Slides of the 55 mn presentation: .pdf (3 MB) to be used with Acrobat Reader.

Bibliographic reference:

\bibitem{Cousot-NYU-2008-04-30}
P.~Cousot.
\newblock Parameterized Refinement in Abstract-Interpretation-Based Static 
          Analysis.
\newblock \emph{Verication group}, Computer Science, NYU, New York, NY, USA, 
          April 20${^\mathrm{th}}$ 2008.

@inProceedings{Cousot-NYU-2008-04-30,
   author =    {P{.} Cousot},
   title =     {Parameterized Refinement in Abstract-Interpretation-Based Static 
                Analysis},
   booktitle = {Verication group},
   address =   {Computer Science, NYU, New York, NY, USA},
   month =     {April 20${^\mathrm{th}}$},
   year =      2008,
}

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