P. Cousot, On Completeness in Abstract Model Checking from the Viewpoint of Abstract Interpretation

Patrick Cousot.
On Completeness in Abstract Model Checking from the Viewpoint of Abstract Interpretation.
Réunion Workshop on Implementations of Logic, Saint Gilles, Réunion Island, November 11, 2000.
Abstract: The notion of abstraction originating from abstract interpretation has been successfully applied in model checking to cope with the state explosion problem for finite state models and to verify infinite state models.
     Contrary to static program analysis applications of abstract interpretation where the abstractions of the program collecting semantics are sound but almost always incomplete (thus leaving out possible cases of uncertainty in the diagnosis), model checking is supposed to be a formal verification method and therefore should only use complete abstractions (allowing only for yes/no answers, all uncertainty resulting only from getting out of computer resources).
     Since, in practice, the manual discovery of such complete abstractions turned out to be difficult, a present stream of research work aims at (partially) automating this discovery of a complete abstraction, e.g. refinement of an initial guess by trial and error.
     We study this problem for the standpoint of abstract interpretation, ignoring time and memory computer resources (hence the term partial completeness) and showing that finding a partially complete abstraction for a model verification is logically equivalent to discovering an inductive argument (e.g. invariant) and checking a proof obligation (in order to verify the soundness of the abstraction). In the context of model-checking, the refinement of abstractions is therefore logically equivalent to the improvement of a proof argument that the model satisfies its specification until this logical argument is inductive, that is satisfies the verification conditions.
Slides of the 45mn talk are available in various formats: .pdf .

\bibitem{Cousot00-Reunion}
P{.} Cousot.
\newblock On Completeness in Abstract Model Checking from the Viewpoint of
Abstract Interpretation.
\newblock \emph{Réunion Workshop on Implementations of Logic}, Saint
Gilles, Réunion Island, November 11, 2000.

@unpublished{Cousot00-Reunion,
   author =  {Cousot, P{.}},
   title =   {On Completeness in Abstract Model Checking from the Viewpoint of Abstract 
              Interpretation},
   note =    {\emph{Réunion Workshop on Implementations of Logic}, Saint Gilles, 
              Réunion Island, November 11, 2000},
}

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