The Prusti Project: Formal Verification for Rust

Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

12 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationNASA Formal Methods
EditorsJyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
PublisherSpringer
Publication date2022
Pages88-108
ISBN (Print)9783031067723
DOIs
Publication statusPublished - 2022
Event14th International Symposium on NASA Formal Methods - Hameetman Center - Caltech Campus, Pasadena, United States
Duration: 24 May 202227 May 2022

Conference

Conference14th International Symposium on NASA Formal Methods
LocationHameetman Center - Caltech Campus
Country/TerritoryUnited States
CityPasadena
Period24/05/202227/05/2022
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13260 LNCS
ISSN0302-9743

Keywords

  • Deductive verification
  • Rust
  • Separation logic

Fingerprint

Dive into the research topics of 'The Prusti Project: Formal Verification for Rust'. Together they form a unique fingerprint.

Cite this