Introduction To SPARK
This tutorial is an interactive introduction to the SPARK programming language and its formal verification tools. You will learn the difference between Ada and SPARK and how to use the various analysis tools that come with SPARK.
This document was prepared by Claire Dross and Yannick Moy.
Note
The code examples in this course use an 80-column limit, which is a typical limit for Ada code. Note that, on devices with a small screen size, some code examples might be difficult to read.
Contents:
- Overview
- Flow Analysis
- Proof of Program Integrity
- State Abstraction
- Proof of Functional Correctness