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