2024-05-13 - SPARK

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.

• Labs

ZIP archive of the labs being done during the class.

Links

• SPARK User Guide

• Abstract Interpretation in a Nutshell

Cousot’s introduction to AbsInt

Schedule

Day	Topic
Day 1	Course Overview Formal Methods and SPARK SPARK Language SPARK Tools Flow Analysis Proof
Day 2	Specification Language Subprogram Contracts Type Contracts Advanced Proof Advanced Flow Analysis SPARK Boundary (intro)
Day 3	Speeding-up Proofs Investigation of Failing Proofs Auto-Active Proof Pointer Programs