Conference paper
The Prusti Project: Formal Verification for Rust
Rust is a modern systems programming language designed to offer both performance and static safety. A key distinguishing feature is a strong type system, which enforces by default that memory is either shared or mutable, but never both. This guarantee is used to prevent common pitfalls such as memory errors and data races.
It can also be used to greatly simplify formal verification, as we demonstrated by developing the Prusti verifier, which can verify rich correctness properties of Rust programs with a very modest annotation overhead. In this paper, we provide an overview of the Prusti project. We outline its main design goals, illustrate examples of its use, and discuss important outcomes from the perspectives of a user, a verification expert, and a tool developer.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2022 |
| Pages: | 88-108 |
| Proceedings: | 14<sup>th</sup> International Symposium on NASA Formal Methods |
| Series: | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| ISBN: | 303106772X , 303106772x , 3031067738 , 9783031067723 and 9783031067730 |
| ISSN: | 16113349 and 03029743 |
| Types: | Conference paper |
| DOI: | 10.1007/978-3-031-06773-0_5 |
| ORCIDs: | Matheja, Christoph |
