![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Friday 30 May 2025, 14:00-15:00
Aeneas: Rust Verification by Functional Translation
- đ¤ Speaker: Son Ho (Azure Research team) đ Website
- đ Date & Time: Friday 30 May 2025, 14:00 - 15:00
- đ Venue: SS03, Computer Laboratory
Abstract
We present Aeneas, a verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to generate pure models for a large class of safe Rust programs which can contain shared and mutable borrows, functions returning borrows, traits and loops. Doing so, we allow the user to reason about the original Rust program through the theorem prover of their choice, and enable lightweight verification by eliminating memory reasoning, allowing them to instead focus on functional properties of their code. As of today, Aeneas has backends for F\*, Coq, HOL4 and most importantly Lean, for which we are investing efforts to develop custom tactics and automation. Aeneas is currently being used to verify optimised, low-level cryptographic code, that we will present as well.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- SS03, Computer Laboratory
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.