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 (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.
