We present the Why/Krakatoa approach to deductive verification of Java programs. Functional behaviors are given in the Java source code, as annotations a la JML. Models can be given using algebraic-style specifications. Verification conditions are generated, whose validity ensures the correctness of source code with respect to the specifications. These are standard first-order formulas, which can be sent to several provers, both interactive ones like Coq or PVS, and automatic ones like Simplify, Yices, or Ergo.
Invited talk at FOOL/WOOD; Saturday, 20 January 2007; Nice, France