P. Cousot, On the Design of Abstractions for Software Model Checking

Patrick Cousot.
On the Design of Abstractions for Software Model Checking.
MicroSoft Research, Seatle, U.S.A., February 12^th, 2001.
Abstract: A lot of work is on-going on the abstract model checking of infinite state models, in particular for the verification of computer software. The idea is to manually design an abstraction of the program semantics in order to get a finite abstract model of program executions, then to use deductive methods in order to prove interactively with a theorem prover or proof checker that the abstract model is a sound abstract interpretation of the program semantics and finally to model-check the finite abstract model using fixpoint computation algorithm.
     In the first part of the talk, we show that up to duality and adjoinedness, this scenario is similar to that of static program analysis but for the use of reusable general-purpose abstractions, manual proofs of correctness and incompleteness (thus leaving out possible cases of uncertainty in the diagnosis).
     In the second part of the talk, we study the partial completeness problem. This consists, up to termination, in designing a sound abstraction which is refined enough to allow for the fixpoint computation/model-checking algorithm to conclude positively that the program is correct.
     We show that the discovery and soundness proof of this abstraction is, for program safety properties, logically equivalent to the program correctness proof itself. This opens a discussion on the practical feasibility of the manual refinement of abstractions.
Slides of the 90mn talk: .pdf (877 Ko) for printing in color.

\bibitem{Cousot01-Microsoft}
P{.} Cousot.
\newblock On the Design of Abstractions for Software Model Checking.
\newblock \emph{MicroSoft, Seatle, U.S.A.}, 
February 12$^{\mathrm{th}}$, 2001.

@unpublished{Cousot01-Microsoft,
   author =  {Cousot, P{.}},
   title =   {On the Design of Abstractions for Software Model Checking},
   note =    {\emph{MicroSoft, Seatle, U.S.A.}, February 12$^{\mathrm{th}}$, 2001},
}

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