Public SPARK Training

Paris, France, Dec 4 - Dec 8, 2017

This in-depth course will cover the SPARK language and formal verification tools through a combination of live lectures and hands-on workshops. Geared towards software engineers and project managers, the course will present the SPARK technology with an emphasis on how to best exploit its benefits in practice. Previous experience with formal verification is not required.

This training course will take place in an 'inter-company' environment in English.

Prerequisite: Knowledge of the Ada programming language (any version of Ada will do)

Each participant should come with a computer.

Trainer: Yannick Moy - SPARK Pro Product Manager

Where

AdaCore, 4th floor
46 rue d’Amsterdam
75009 Paris

Time

0930 – 1700

Lunch Break

1230 – 1400

AdaCore Contact

Eric Perlade
+33 1 49 70 87 58 // +33 6 30 85 65 51

Day 1

  • SPARK 2014 Introduction
  • Functional contracts in Ada 2012 and SPARK 2014

Day 2

  • Flow analysis
  • Proof of program integrity

Day 3

  • State abstraction
  • Proof of functional correctness

Day 4

  • Systems programming
  • Concurrency
  • Object Oriented programming

Day 5

  • Using ghost code
  • Combining test and proof
  • Levels of Software Assurance