Session
FOSDEM 2021 Schedule
Safety and Open Source

Adding contracts to the GCC GNAT Ada standard libraries

to strengthen analysis provided by formal verification tools
D.safety
Joffrey Huguet
The guarantees provided by SPARK, an open-source formal proof tool for Ada, and its analysis are only as strong as the properties that were initially specified. In particular, use of third-party libraries or the Ada standard libraries may weaken the analysis, if the relevant properties of the library API are not specified. We progressively added contracts to some of the GCC GNAT Ada standard libraries to enable users to prove additional properties when using them, thus increasing the safety of their programs. In this talk, I will present the different levels of insurance those contracts can provide, from preventing some run-time errors to occur, to describing entirely their action.

Additional information

Type devroom

More sessions

2/6/21
Network monitoring, discovery and inventory
Stephan Schmidt
D.network
A brief introduction to the room and to the sessions.
2/6/21
Hardware-Aided Trusted Computing
Jo Van Bulck
D.hardware.trusted
A brief introduction to the room and to the sessions.
2/6/21
MariaDB
Ian Gilfillan
D.mariadb
A brief introduction and overview of what you can expect from the MariaDB devroom at FOSDEM
2/6/21
Microkernel
Martin Děcký
D.microkernel
Welcome talk and introduction to the Microkernel Devroom at FOSDEM 2021.
2/6/21
Testing and Automation
D.testing
A warm welcome from your devroom managers, practical information, lineup and administrivia. Let's make this edition of FOSDEM count! Happy Testing!
2/6/21
OpenPOWER
Toshaan Bharvani
D.power
This will be an introduction to the OpenPOWER community and the OpenPOWER foundation.
2/6/21
Perl and Raku Programming
D.perl
A brief introduction to the 2021 virtual FOSDEM devroom, talk overview, code of conduct and Community Affairs Team