Linear Ghost Types Are All You Need - An Introduction to Proof-Oriented Programming in Verus
Aus International Center for Computational Logic
Linear Ghost Types Are All You Need - An Introduction to Proof-Oriented Programming in Verus
Verteidigung Studienarbeit von Matthias Meißner
- Veranstaltungsort: APB 3027
- Beginn: 11. September 2025 um 11:00
- Ende: 11. September 2025 um 12:00
- Forschungsgruppe: Wissensbasierte Systeme
- Event series: Research Seminar Logic and AI
- iCal
Previously in this seminar, we introduced a concurrent separation logic (IRIS) to verify the memory safety of unsafe code inside Rust's standard library. Conversely, the observation that the safe subset of Rust can be efficiently encoded into constraint horn clauses has led to highly automated, SMT-solver based tools for the verification of this subset of rust. Naturally, the next question is how to automate the verification of Rust programs that do use unsafe code. Linear ghost types offer a simple yet powerful solution: We can reuse the borrow checking that is already performed by the Rust compiler to automate a separation logic built into the source code, allowing for a "proof oriented programming" style. In this talk, we show how linear ghost types relate to the broader landscape of verification tools for Rust and how to use them for the verification of low level data structures -- an application which might be useful for nemo, the Rust-based logic reasoner developed in our group.
