Creusot, a prophetic verifier for Rust

Xavier Denis (University of Paris-Saclay, France) will give an talk, in person and online, for the Huawei – Edinburgh Coffee House Tech Talk Series. The details of the talk are below.

*When*: Tuesday 26 April 2022 at 11am

*Where* (in person): Huawei Edinburgh Research Centre (2 Semple Street, 5th floor, Meeting Room 1, Edinburgh EH3 8BL)

*Where* (virtually): via Zhumu link (https://meeting.zhumu.me/wc/0616463788/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0 ), everybody is welcome!

You can access it from your own browser, without installing anything.

*Speaker*: Dr. Xavier Denis (University of Paris-Saclay, France)

*Title*: Creusot, a prophetic verifier for Rust

*Abstract*:

Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification, which aims at proving the conformity of Rust code with respect to a specification of its intended behavior. We present Creusot, a tool for the formal specification and deductive verification of Rust. Creusot’s specification language features a notion of prophecies to reason about memory mutation. Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code.

The support for traits is at the heart of Creusot’s approach of verification and specification of programs.

*Brief speaker bio*:

Xavier Denis is a PhD student at the LMF in Paris where he works on developing a pragmatic verifier for Rust software. Before his studies he was a Site Reliability Engineer where he gained an appreciation for the impact of bugs on real-world software.