• Compressed PostScript .ps.gz (144 Kb),
• PDF (132 Kb)

• in the verification that the semantics of a computer system satisfies a specification (showing the rôle of agregation, transition, input-output and reachability abstractions in abstract proofs);
• in the verification of programs by static analysis (discussing the rôle of property versus model-based abstractions, program versus language-based abstractions, local versus global abstractions, single versus multiple abstractions, and discussing the design of abstractions by reduction and refinement);
• in soundness, completeness and adequation of abstractions.

• A4 landscape .pdf (996 Kb) for viewing with Acrobate Reader and compressed PostScript .ps.gz (5.9 Mb) for viewing with Ghostview or printing;
• 2 slides per A4 portrait page .pdf (568 Kb) for viewing with Acrobate Reader and compressed PostScript .ps.gz (3.8 Mb) for viewing with Ghostview or printing;
• 4 slides per A4 landscape sheet for printing, .ps.gz (424 Kb), .ps.gz (2.6 Mb).

     

\bibitem{Cousot07-SEFM}
P.~Cousot.
\newblock The R\^ole of Abstract Interpretation in Formal Methods (Keynote 
          Talk).
\newblock In \emph{Proc. IEEE International Conference on Software 
          Engineering and Formal Methods}, M.~Hinchey and T.~Margaria (Eds.), 
          London, UK, September 12--14, 2007, IEEE Press, pages 135--137, 

@inproceedings{Cousot07-SEFM,
   author =    {P{.} Cousot},
   title =     {The R\^ole of Abstract Interpretation in Formal Methods},
   booktitle = {Proc. IEEE International Conference on Software 
                Engineering and Formal Methods},
   editor =    {M.~Hinchey and T.~Margaria},
   address =   {London, UK},
   month =     sep # " 10--14",
   publisher = {IEEE Press},
   pages =     {135--137},
   year =      2007,
}