Introduction to Formal Verification with SPARK

How to prove safety and security for embedded and systems software using SPARK Pro.

In this session, you'll learn about what SPARK is, how SPARK works, and see how SPARK can be applied to a M.A.R.S. Rover to prove safety.

We’ll cover:

What is SPARK?

• Deductive program verification for the SPARK language - an Ada-derived language with broad coverage of Ada features
• Practical, modular, scalable verification for systems and embedded programs
• Professional, industrial-strength formal methods

What’s it like to use SPARK?

• Building a safety monitor for a M.A.R.S. Rover
• Automatic proof for the autonomous mode
• Discovery of an error in the remote-control mode

The Future: SPARK and Generative AI

• SPARK: the best possible language to use for Generative AI