reposiTUm: Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust

Record link:

http://hdl.handle.net/20.500.12708/227859
https://doi.org/10.34726/12079

Title:

Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust

Citation:

Sextl, F. (2026, April 13). Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust [Presentation]. Sixth Rust Verification Workshop (RW2026), Turin, Italy. https://doi.org/10.34726/12079

reposiTUm DOI:

10.34726/12079

Publication Type:

Presentation - Presentation

Language:

English

Authors:

Sextl, Florian

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering
E056-13 - Fachbereich LogiCS

Date (published):

13-Apr-2026

Event name:

Sixth Rust Verification Workshop (RW2026)

Event date:

13-Apr-2026 - 14-Apr-2026

Event place:

Turin, Italy

Keywords:

Rust; memory safety; Biabduction

Abstract:

This talk introduces a new prototype tool implementing biabduction-based shape analysis for unsafe Rust. It first motivates the need for automated safety requirements synthesis for unsafe Rust, then gives a short introduction to biabduction-based shape analysis, and lastly presents the new tool (with a demo).

Project title:

Verification and Analysis for Safety and Security of Applications in Life: 101160022 (European Commission)

Project (external):

European Union Horizon 2020

Project ID:

101034440

Link (external):

https://codeberg.org/firefighterduck/Brush_rs

Research Areas:

Logic and Computation: 100%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%