IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2022 > Flux: Liquid Types for Rust
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Nico Lehmann

martes 4 de octubre de 2022

11:00am Zoom3 - (pass: @s3)

Nico Lehmann, PhD Student, UC San Diego

Flux: Liquid Types for Rust


Low-level pointer-manipulating programs are hard to verify, requiring complex spatial program logics that support reasoning about aliasing and separation. Worse, when working over collections, these logics burden the programmer with annotating loops with quantified invariants that describe the contents of the collection. In this talk, I will give a demo of Flux, a static verifier for Rust that shows how logical refinements can work hand in glove with Rust’s ownership mechanisms to yield ergonomic type-based verification for low-level imperative code. By factoring complex invariants into type constructors and simple refinements, Flux can efficiently synthesize loop annotations via liquid inference. We use a suite of vector-manipulating programs to demonstrate the advantages of Flux’s refinement types over program logics, as implemented in the state-of-the-art Prusti verifier.