Title
Flux: Liquid Types for Rust

Abstract
Low-level, pointer-manipulating programs are tricky to write and devilishly hard to verify, requiring complex spatial program logics to reason about heap updates. Recent systems like Prusti and Creusot take advantage…