In the second part of the talk, we compare program static analysis with deductive methods, model-checking and type inference. Their foundational ideas are shortly reviewed, and the shortcomings of these four tools are discussed, including when they are combined. Alternatively, since program debugging is still the main program verification method used in industry, we suggest to combine formal with informal methods.

Finally, the grand challenge for all formal methods and tools is to solve the software reliability, trustworthiness or robustness problems. Few challenges more specific to program analysis by abstract interpretation are shortly discussed.

The published slides slightly extend those of the presentation and include a shortened bibliography, mainly restricted to result obtained in our research group.

\bibitem{Cousot00-Dagstuhl-Talk}
P{.} Cousot.
\newblock Progress on Abstract Interpretation Based Formal Methods and
Future Challenges.
\newblock Conference at the Occasion of Dagstuhl's 10th Anniversary,
“Informatics --- 10 Years Back, 10 Years Ahead”, Saarland
University Campus, Saarbrücken, Germany, August 28-31, 2000.

@unpublished{Cousot00-Dagstuhl-Talk,
   author =  {Cousot, P{.}},
   title =   {Progress on Abstract Interpretation Based Formal Methods and
              Future Challenges},
   note =    {Conference at the Occasion of Dagstuhl's 10th Anniversary,
              “Informatics --- 10 Years Back, 10 Years Ahead”,
              Saarland University Campus, Saarbrücken, Germany},
   month =   {28--31 \aug},
   year =    2000,
}