Session
FOSDEM Schedule 2021
Safety and Open Source

Proving heap-manipulating programs with SPARK

The SPARK open-source proof tool for Ada now supports verifying pointer-based algorithms thanks to an ownership policy inspired by Rust
D.safety
Claire Dross
SPARK is an open-source tool for formal verification of the Ada. language. Last year, support for pointers, aka access types, was added to SPARK. It works by enforcing an ownership policy somewhat similar to the one used in Rust. It ensures in particular that there is only one owner of a given data at all time, which can be used to modify it. One of the most complex parts for verification is the notion of borrowing. It allows to transfer the ownership of a part of a data-structure, but only for a limited time. Afterward ownership returns to the initial owner. In this talk, I will explain how this can be achieved and, in particular, how we can describe in the specification the relation between the borrower and the borrowed object at all times.

Additional information

Type devroom

More sessions

2/6/21
Emulator Development
Mahmoud Abdelghany
D.emulator
Thank you, and good night Emulator Development Room
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.