2025-05-20 - 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 Flow Analysis
Day 2	Proof Specification Language Subprogram Contracts Type Contracts Advanced Proof
Day 3	Advanced Flow Analysis Pointer Programs Auto-Active Proof State Abstraction SPARK Boundary
Day 4	SPARK Example Project

Documentation

• SPARK Reference Manual

• SPARK User’s Guide

• Ada Reference Manual

• GNAT Reference Manual

• GNAT User Guide