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 ( ), 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


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.



Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.