CP 2016 has ended
Back To Schedule
Monday, September 5 • 09:00 - 09:35
CP meets Verification - Invited talk: Challenges of Program Verification with SPARK
    See presentations
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.

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 →

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

Attendees (2)