BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Aeneas: Rust Verification by Functional Translation - Son Ho (Azur
 e Research team)
DTSTART:20250530T130000Z
DTEND:20250530T140000Z
UID:TALK232588@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:We present Aeneas\, a verification toolchain for Rust programs
  based on a\nlightweight functional translation.\nWe leverage Rust's rich 
 region-based type system to generate pure models for a large class\nof saf
 e Rust programs which can contain shared and mutable borrows\, functions r
 eturning\nborrows\, traits and loops.\nDoing so\, we allow the user to rea
 son about the original Rust program through the theorem\nprover of their c
 hoice\, and enable lightweight verification by eliminating memory\nreasoni
 ng\, allowing them to instead focus on *functional* properties of their co
 de.\nAs of today\, Aeneas has backends for F\\*\, Coq\, HOL4 and most impo
 rtantly Lean\, for which\nwe are investing efforts to develop custom tacti
 cs and automation. Aeneas is currently\nbeing used to verify optimised\, l
 ow-level cryptographic code\, that we will\npresent as well.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR