General Informations

Research and Teaching

Online Resources

Tutorial 2
Introduction to SPARK~2014 - How to Develop Ultra-Low Defect Software

Monday 18th September, 11.00 - 12.30
Organizer: Martin Becker (Technische Universitat Munchen, Germany)

This tutorial aims at giving a practical, hands-on introduction to SPARK 2014, a modern, imperative and object-oriented programming language, specifically conceived for the development and formal verification of high-integrity software.
We cover basic features of the language, such as data types, concurrency and contracts, and then apply static verification to prove the correctness of contracts, as well as the absence of run-time errors (such as overflows, division by zero or even race conditions). Further topics include the inclusion of legacy code, the combination of testing and static analysis, the precision of numerical operations, and a brief outlook on secure programming for data-sensitive applications. We close the tutorial with an example of how these tools can be used in a practical setting.


Participants should bring a laptop with GNAT GPL and SPARK GPL installed (download for free from, to be able to follow the exercises.

<< Back to hands-on tutorials