• adequacy of the concrete semantics (choice of primitives, mathematical versus computer-based definition, etc),
• nature of the abstraction (relational, non-relational, parametric, etc.) and its computer encoding,
• soundness of the abstraction and the abstract verification conditions (so that no later inference can lead to erroneous conclusions such as false positives),
• correct and effective induction (that is how inductive invariants are computed by concrete/abstract iteration with extrapolation, constraint solving, abstraction/refinement, elimination, exact resolution, etc),
• ability to scale up (for programs in the small to programs in the large, separate abstractions, etc), and
• precision of the abstraction (to avoid false alarms).

• PostScript: 1/1 .ps.gz, 2/1 .ps.gz, < href="http://www.di.ens.fr/%7Ecousot/publications.www/slides/Cousot-2008-06-03--06-NSV08_4-1.ps.gz">4/1 .ps.gz for viewing with GhostScript and GhostView or (color) printing;
• PDF: 1/1 .pdf, 2/1 .pdf, 4/1 .pdf to be used with Acrobat Reader.

\bibitem{Cousot08-NSV}
P. Cousot.
\newblock Numerical domains for software verification by abstract 
          interpretation, invited talk.
\newblock First International Workshop on Numerical Abstractions for Software 
          Verification, NSV 2008, Princeton, New Jersey, USA, July 8th, 2008.

@unpublished{Cousot08-NSV,
   author =    {P{.} Cousot},
   title =     {Numerical domains for software verification by abstract
               interpretation, invited talk},
   note =      {First International Workshop on Numerical Abstractions for Software 
                Verification, NSV 2008},
   month =     "8 " # jul,
   year =      2008,
}