Tutorial: Get Started with Formal Methods for Safety and Security Using SPARK

Olivier Henley, AdaCore, Canada

Ada SPARK is a language that enables formal deductive verification, allowing developers to statically prove the absence of runtime errors as well as functional correctness. Join us in this half day tutorial where we start from scratch to install our toolchain, integrate with VS Code and then use AI to generate a first version of our program. We then incrementally use formal verification to prove the absence of runtime errors and lastly functional correctness and optionally run our program on a Raspberry Pi Pico.

SPARK is a subset of Ada, which means that programmers can use all of the Ada ecosystem, from IDE plugins, to libraries to hardware and OS or baremetal support.

The objective of the workshop is to demonstrate that SPARK enables developers to utilize formal methods to improve the safety and security of their code. No previous Ada or SPARK knowledge required.

Presentation topics

• Formal verification in SPARK
• Incrementally improving the extent of the proof
• Using AI to generate programs and proofs
• The Alire package manager to manage dependencies
• Ada runtimes to execute directly on embedded boards

Duration: half-day

Level: Introductory, experience in programming required, laptop required (Windows, Mac or Linux).

Presenter

The author, Olivier Henley, is a UX Engineer at AdaCore. His role is exploring new markets through technical stories. Prior to joining AdaCore, Olivier was a consultant software engineer for Autodesk. Prior to that, Olivier worked on AAA game titles such as For Honor and Rainbow Six Siege in addition to many R&D gaming endeavors at Ubisoft Montreal. Olivier graduated from the Electrical Engineering program at Polytechnique Montreal. He is a co-author of patent US8884949B1, describing the invention of a novel temporal filter implicating NI technology. An Ada advocate, Olivier actively curates GitHub’s Awesome-Ada list.