Seminar details

Room 206 (2nd floor, badged access)

24 November 2022 - 14h00
Deductive Verification of Higher-Order Rust Programs
by Xavier Denis from 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 ( 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 | Site Map | Site powered by SPIP 3.2.16 + AHUNTSIC [CC License]

info visites 1922210