AdaCore University

Ada 006

SPARK 2014

Get Started

SPARK 2014 overview

SPARK 2014 is a language based on Ada 2012, allowing for formal verification. This course will describe the language subset together with the tools and techniques allowing to formally defining properties and verifying their correctness.

Lesson Index

  1. SPARK 2014 overview
  2. SPARK 2014 Flow Analysis
  3. SPARK 2014 Proof of Program Integrity
  4. SPARK 2014 State Abstraction
  5. SPARK 2014 Proof of Functional Correctness

Course Prerequisites