On Monday, we had a kickoff event for the ProofInUse joint lab between Inria and AdaCore. The slides of presentations are now available on the page of the event.
The main take home message for me is that teams developing SMT solvers (in particular Alt-Ergo and CVC4) are willing to invest substantial efforts on supporting much more efficiently the theories of bitvectors and floats that are very important for proof of programs. And we'll make sure as part of ProofInUse work to tailor the generation of VCs in Why3 to each prover's strengths, adding support as needed in Why3 language, libraries and platform. Not only this means that SPARK users will be able to prove their programs more automatically, but Frama-C or Atelier B users as well, provided the developers of these tools also adapt their use of Why3 to benefit from these improvements.