The RustBelt and its Separation Logic
Aus International Center for Computational Logic
The RustBelt and its Separation Logic
Vortrag von Matthias Meißner
- Veranstaltungsort: APB 3027
- Beginn: 28. November 2024 um 11:00
- Ende: 28. November 2024 um 12:00
- Forschungsgruppe: Wissensbasierte Systeme
- 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.
