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.