Proving Software Security with SPARK Pro
In this webinar, Yannick Moy outlines key features of SPARK Pro for proving that code obeys its specification, including the language to express this specification, and the process to successfully prove compliance.
You'll learn more about:
- The powerful specification language in SPARK
- Expressing natural language specifications as contracts in the code
- How special “ghost” code can help with specification
- How to use ghost code to develop proofs as code
- How SPARK Pro supports the user with detailed feedback
Authors
M. Anthony Aiello
Tony Aiello is a Product Manager at AdaCore. Currently, he manages SPARK Pro, GNAT Pro for Rust, and GNAT IQ.
Yannick Moy
Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.
