Joffrey Huguet
Type devroom
to strengthen analysis provided by formal verification tools
Starts on day 1 (2021-02-06) at 11:00 (Brussels time, UTC+1) in room Safety (duration 00:30)
Matrix room #safety:fosdem.org
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.
=> FOSDEM schedule page This content has been proxied by September (3851b).Proxy Information
text/gemini; lang=en