2025-06-23 - SPARK Essentials

This page contains links to everything you will need for this training class.

Files

• Slides

This is a PDF copy of the slides presented during the course.

• Lab Source

These are starting points for the class labs.

• Lab Answers

These are answers for the class labs.

Schedule

Day	Topic
Day 1	Course Overview Formal Methods and SPARK SPARK Language SPARK Tools
Day 2	Flow Analysis Proof Specification Language Subprogram Contracts
Day 3	Type Contracts Advanced Proof Advanced Flow Analysis Pointer Programs
Day 4	Auto-Active Proof State Abstraction SPARK Boundary SPARK Example Project

Documentation

• SPARK Reference Manual

• SPARK User’s Guide

• Ada Reference Manual

• GNAT Reference Manual

• GNAT User Guide