Détails sur le séminaire


Room 206 (2nd floor, badged access)

24 novembre 2022 - 14h00
Deductive Verification of Higher-Order Rust Programs
par Xavier Denis de LRI



Abstract: The Rust language aims to empower systems software programmers by offering them safe, and powerful linguistic abstractions to solve their problems. One of the most important are iterators which provide a composable mechanism to express traversal and modification of structures. However when verifying code iterators pose many problems, they can be non-deterministic, infinite, higher-order, and effectful.

Creusot (https://github.com/xldenis/creusot) is a state-of-the-art verification platform for safe Rust code, it leverages the Rust type system to simplify verification, giving Rust programs mutable value semantics.

In this talk we use Creusot to construct a general, composable, framework to verify iterators and their clients.
We motivate this with several key examples: IterMut the type of mutable iterators over slices, and Map the iterator which performs a functional `map` using a mutable closure.

We also provide an introduction to reasoning and verification in Creusot.




Contact | Plan du site | Site réalisé avec SPIP 3.2.16 + AHUNTSIC [CC License]

info visites 1919749