P. Cousot, Automatic Verification by Abstract Interpretation

Patrick Cousot.
Automatic Verification by Abstract Interpretation.
International Symposium in Honor of Zohar Manna, Taormina, Sicily, Italy, June 29—July 4, 2003.
Abstract:
     The idea of “abstraction”, as formally introduced by the theory of abstract interpretation, as been recognized to be a key to program verification.
     Unfortunately, it is often understood in a finitary way, e.g. in (abstract) software model checking, in order to be able to reuse existing model checkers and as state-wise abstraction, which eliminates many expressive alternatives. Therefore, in a first part, we recall some fundamental and well-known results in abstract interpretation, showing the limits of these restricted approaches. This is applied to predicate abstraction with refinement, which inherent limitations are explained in light of these basic results in abstract interpretation theory. In particular, we show that simple constant propagation methods are out of its scope.
     In a second part, we eliminate these limitations, using infinitary abstractions with widening/narrowing, showing how generic abstract domains can be used to verify families of programs without requiring the user to provide specific invariant predicates for each particular program in the family.
Slides of the 30 mn talk are available in 4 slides per A4 landscape sheet format .pdf.gz

Bibliography:

\bibitem{Cousot03-Zohar}
P{.} Cousot.
\newblock Automatic verification by abstract interpretation, Invited talk.
\newblock \emph{International Symposium in Honor of Zohar Manna},
	  Taormina, Sicily, Italy, Tuesday, July 1$^{\textrm{st}}$, 2003.

@unpublished{Cousot03-Zohar,
   author =  {P{.} Cousot},
   title = {Automatic verification by abstract interpretation, Invited talk},
   note = {\emph{International Symposium in Honor of Zohar Manna},
	   Taormina, Sicily, Italy, Tuesday, July 1$^{\textrm{st}}$, 2003},
}

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