CP 2016 has ended
Back To Schedule
Monday, September 5 • 09:00 - 10:00
CP meets Verification Workshop
  • 09:00. Openning
  • 09:00 - 09:35. Invited talk: Challenges of Program Verification with SPARK, Yannick Moy. Abstract: SPARK is an industrially supported formal verification toolset for critical software written in the Ada programming language. SPARK technology is based on the Why3 intermediate language and toolset for formal program verification, and the Alt-Ergo, CVC4 and Z3 automatic provers. SPARK is used to formally verify properties of critical software ranging from absence of run-time errors to functional correctness. Current challenges for automatic proof are the ability to deal with nonlinear arithmetic, conversions between types (bitvectors, integers, floats, reals), handling of floating-point arithmetic and the combination of all these with quantification arising from both user specifications and the encoding of programming language specifications. We present the achievements of current projects ProofInUse and SOPRANO, and the roadmap for better use of automatic provers in formal program verification.
  • 09:35 - 10:00. Regular talk: Mixing Polyedra and Boxes Abstract Domain for Constraint Solving, Marie Pelleau, Emmanuel Rauzy, Ghiles Ziat, Charlotte Truchet, Antoine Miné.

avatar for Yannick Moy

Yannick Moy

Senior Software Engineer, AdaCore SAS
Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments... Read More →
avatar for Marie Pelleau

Marie Pelleau

UPMC - Lip6

Monday September 5, 2016 09:00 - 10:00
B202 Bosco building

Attendees (2)