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


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

0930 – 1700

Lunch Break
1230 – 1400

AdaCore Contact
Eric Perlade

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

Email Eric Perlade

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

If you are interested in the event you may register using the form below. For more information about the event or pricing info contact us at

After you register for this course we will send you instructions for downloading the AdaCore software that will be used for the workshops. Please pre-install these files on your laptop and bring it with you to the course.