RustyDL: A Program Logic for Rust
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912926954160128 |
|---|---|
| author | Drodt, Daniel Hähnle, Reiner |
| author_facet | Drodt, Daniel Hähnle, Reiner |
| contents | Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool for Rust. RustyDL reasons about Rust programs directly on the source code level, in contrast to other tools that are all based on translation to an intermediate language. A source-level program logic for Rust is crucial for a human-in-the-loop (HIL) style of verification that permits proving highly complex functional properties. We discuss specific Rust challenges in designing a program logic and calculus for HIL-style verification and propose a solution in each case. We provide a proof-of-concept of our ideas in the form of a prototype of a Rust instance of the deductive verification tool KeY. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_22075 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | RustyDL: A Program Logic for Rust Drodt, Daniel Hähnle, Reiner Programming Languages Logic in Computer Science 68Q60 Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool for Rust. RustyDL reasons about Rust programs directly on the source code level, in contrast to other tools that are all based on translation to an intermediate language. A source-level program logic for Rust is crucial for a human-in-the-loop (HIL) style of verification that permits proving highly complex functional properties. We discuss specific Rust challenges in designing a program logic and calculus for HIL-style verification and propose a solution in each case. We provide a proof-of-concept of our ideas in the form of a prototype of a Rust instance of the deductive verification tool KeY. |
| title | RustyDL: A Program Logic for Rust |
| topic | Programming Languages Logic in Computer Science 68Q60 |
| url | https://arxiv.org/abs/2602.22075 |