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

Patrick Cousot.
Introduction to a Discussion on Mechanical Formal Methods for Software Verification.
IFIP WG 2.3 Meeting, Santa Cruz, California, U.S.A., January 7--12, 2001.
Abstract: As an introduction to a discussion on the effectiveness of mechanical formal methods for software verification, we shortly review the foundational ideas and shortcomings of program typing, static program analysis, abstract model checking, deductive methods as well as combinations of these mechanical formal methods.
As a possible alternative to these mechanical formal methods, we propose a combination of formal and informal methods in the form of abstract program testing which is similar to debugging but for the replacement of program execution on actual data by an abstract interpretation of the program on abstract properties (chosen by the user in a predefined set of abstract domains) in order to check user-defined abstract temporal properties (with yes, no or uncertain answers due to the approximation introduced by the abstraction).
To start the discussion, we question the feasibility of mechanical formal methods and claim that abstract program testing, which is close to debugging hence to programmers's ability, is likely to be a successful breakthrough.
Slides of the 90mn talk (with ongoing discussion): .pdf

\bibitem{Cousot01-SantaCruzB}
P{.} Cousot.
\newblock Introduction to a Discussion on Mechanical Formal Methods for
Software Verification.
\newblock \emph{IFIP WG 2.3 Meeting, Santa Cruz, California, U.S.A.}, 
January 7--12, 2001.

@unpublished{Cousot01-SantaCruzB,
   author =  {Cousot, P{.}},
   title = {Introduction to a Discussion on Mechanical Formal Methods for
   Software Verification},
   note =    {\emph{IFIP WG 2.3 Meeting, Santa Cruz, California, U.S.A.}, January
              7--12, 2001},
}

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