P. Cousot, On Abstraction in Software Verification

Patrick Cousot.
On Abstraction in Software Verification, CAV 2002 invited tutorial.
International Conference on Computer-Aided Verification (CAV 2002), Copenhagen, Denmark, July 27-31, 2002.
Abstract:      Our objective in this talk is to give an intuitive account of abstract interpretation theory and to present and discuss its application to formal methods and in particular to static abstract software checking.
     We start with a discussion of formal methods and computer-aided verification and motivate their formalization by abstract interpretation. Then we informally introduce abstract interpretation and present a few basic elements of the theory.
     Abstract interpretation theory formalizes the conservative approximation of the semantics of hardware or software computer systems. The semantics provides a formal model describing all possible behaviors of a computer system in interaction with any possible environment. By approximation we mean the observation of the semantics at some level of abstraction, ignoring irrelevant details. Conservative means that the approximation can never lead to an erroneous conclusion.
     Abstract interpretation theory provides thinking tools since the idea of abstraction by conservative approximation is central to reasoning (in particular on computer systems) and mechanical tools since the idea of an effectively computable approximation leads to a systematic and constructive formal design methodology of automatic semantics-based program manipulation algorithms and tools.
     We will present various applications of abstract interpretation theory to the design of hierarchies of semantics, program transformations, typing, model-checking and in more details static program analysis.
     We show that their always exists an abstraction into a small finite boolean domain to prove any safety property of a single program by fixpoint/model checking. However the design of the model and its soundness proof is logically equivalent to a formal proof. This shows that model-checking is always feasible, that the only difficulty is to design a model and that this model can always be designed by abstraction of the operational semantics of the program to be checked.
     The whole problematics of static analysis is to automate the design of this abstract model/semantics. For the static analysis of a full programming language, no such finite abstraction exists, so that infinite abstract domains and widenings are needed and more powerful than finite abstractions. We finally discuss the design of program static analyzers and report on an ongoing experience with the design of a parametric specializable program static analyzer for safety-critical real-time embedded software.
Slides of the 120mn talk:.pdf.gz;

Bibliography:

\bibitem{Cousot02-CAV}
P{.} Cousot.
\newblock On Abstraction in Software Verification, Invited tutorial.
\newblock \emph{International ConferenceÊon Computer-AidedÊVerification}
          (CAV 2002), Copenhagen,ÊDenmark, Saturday, July 27, 2002.

@unpublished{Cousot02-CAV,
   author =  {P{.} Cousot},
   title = {On Abstraction in Software Verification, Invited tutorial},
   note = {\emph{International ConferenceÊon Computer-AidedÊVerification}
           (CAV 2002), Copenhagen,ÊDenmark, Saturday, July 27, 2002},
}

copyright notice.
Last modified: Monday, 07-May-2012 17:56:40 EDT