Loading…
This event has ended. View the official site or create your own event → Check it out
This event has ended. Create your own
View analytic
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.

Moderators
Speakers
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 of SPARK 2014, a product he presents in articles, conferences, classes and blogs (in particular www.spark-2014.org). Yannick previously worked on source code... Read More →


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

Attendees (2)