The RustBelt and its Separation Logic
From International Center for Computational Logic
The RustBelt and its Separation Logic
Talk by Matthias Meißner
- Location: APB 3027
- Start: 28. November 2024 at 11:00 am
- End: 28. November 2024 at 12:00 pm
- Research group: Knowledge-Based Systems
- Event series: Research Seminar Logic and AI
- iCal
Rust is a systems-programming language whose expressive type system centers around the concept of ownership enabling both stronger, statically verified safety guarantees as well as lower level control compared to more mainstream "safe" languages. The RustBelt project provided some formal verification for those claims using a seperation logic for modelling rusts typing rules. In this seminar we aim at giving an introduction into the features of Rust's type system as well as into the stack of logical tools used to verify the properties it promises.
