Yannick Moy, AdaCore
From 12.00 until 13.30
At CNB/F/110 (Lunch) + CNB/F/100.9 (Seminar), ETH Zurich
Universitätstrasse 6, 8092 Zurich
Abstract:
The SPARK open source technology developed and commercialized by AdaCore (since 2008) and Altran (since 1987) is both a programming language and formal program verification toolset aimed at the highest levels of software assurance. In this presentation, we will give an overview of the SPARK Ada language and SPARK proof technology, focusing on its use for developing secure software. In particular, we will detail the challenges for industrial use of such technology, and how they were addressed in the most recent version of the technology. A special focus will be put on how we prevent and detect unsoundness in the toolchain, which has the potential to invalidate the guarantees obtained with formal verification. We will give examples of open source projects using SPARK to develop secure software, and do a demo of the tools.