💾 Archived View for gemini.bortzmeyer.org › fosdem › event-11077.gmi captured on 2022-04-29 at 01:32:39. Gemini links have been rewritten to link to archived content

View Raw

More Information

⬅️ Previous capture (2021-12-17)

-=-=-=-=-=-=-

FOSDEM event "Proving heap-manipulating programs with SPARK"

Claire Dross

Type devroom

The SPARK open-source proof tool for Ada now supports verifying pointer-based algorithms thanks to an ownership policy inspired by Rust

Starts on day 1 (2021-02-06) at 13:30 (Brussels time, UTC+1) in room Safety (duration 01:00)

Matrix room #safety:fosdem.org

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.

FOSDEM schedule page