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

doi:10.1007/978-3-031-06773-0_5

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 proceeding › Article in proceedings › Research › peer-review

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 language	English
Title of host publication	NASA Formal Methods
Editors	Jyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
Publisher	Springer
Publication date	2022
Pages	88-108
ISBN (Print)	9783031067723
DOIs	https://doi.org/10.1007/978-3-031-06773-0_5
Publication status	Published - 2022
Event	14^th International Symposium on NASA Formal Methods - Hameetman Center - Caltech Campus, Pasadena, United States Duration: 24 May 2022 → 27 May 2022

Conference

Conference	14^th International Symposium on NASA Formal Methods
Location	Hameetman Center - Caltech Campus
Country/Territory	United States
City	Pasadena
Period	24/05/2022 → 27/05/2022

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13260 LNCS
ISSN	0302-9743

Keywords

Deductive verification
Rust
Separation logic

Access to Document

10.1007/978-3-031-06773-0_5

OpenUrl availability

Full text

Cite this

Astrauskas, V., Bílý, A., Fiala, J., Grannan, Z., Matheja, C., Müller, P., Poli, F., & Summers, A. J. (2022). The Prusti Project: Formal Verification for Rust. In J. V. Deshmukh, K. Havelund, & I. Perez (Eds.), NASA Formal Methods (pp. 88-108). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 13260 LNCS https://doi.org/10.1007/978-3-031-06773-0_5

Astrauskas, Vytautas ; Bílý, Aurel ; Fiala, Jonáš et al. / The Prusti Project : Formal Verification for Rust. NASA Formal Methods . editor / Jyotirmoy V. Deshmukh ; Klaus Havelund ; Ivan Perez. Springer, 2022. pp. 88-108 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13260 LNCS).

@inproceedings{5dd8818ec9524c0993b2ea030240954a,

title = "The Prusti Project: Formal Verification for Rust",

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.",

keywords = "Deductive verification, Rust, Separation logic",

author = "Vytautas Astrauskas and Aurel B{\'i}l{\'y} and Jon{\'a}{\v s} Fiala and Zachary Grannan and Christoph Matheja and Peter M{\"u}ller and Federico Poli and Summers, {Alexander J.}",

note = "Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 14<sup>th</sup> International Symposium on NASA Formal Methods, NFM 2022 ; Conference date: 24-05-2022 Through 27-05-2022",

year = "2022",

doi = "10.1007/978-3-031-06773-0_5",

language = "English",

isbn = "9783031067723",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "88--108",

editor = "Deshmukh, {Jyotirmoy V.} and Klaus Havelund and Ivan Perez",

booktitle = "NASA Formal Methods",

}

Astrauskas, V, Bílý, A, Fiala, J, Grannan, Z, Matheja, C, Müller, P, Poli, F & Summers, AJ 2022, The Prusti Project: Formal Verification for Rust. in JV Deshmukh, K Havelund & I Perez (eds), NASA Formal Methods . Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13260 LNCS, pp. 88-108, 14^th International Symposium on NASA Formal Methods, Pasadena, California, United States, 24/05/2022. https://doi.org/10.1007/978-3-031-06773-0_5

The Prusti Project : Formal Verification for Rust. / Astrauskas, Vytautas; Bílý, Aurel; Fiala, Jonáš et al.

NASA Formal Methods . ed. / Jyotirmoy V. Deshmukh; Klaus Havelund; Ivan Perez. Springer, 2022. p. 88-108 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13260 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - The Prusti Project

T2 - 14<sup>th</sup> International Symposium on NASA Formal Methods

AU - Astrauskas, Vytautas

AU - Bílý, Aurel

AU - Fiala, Jonáš

AU - Grannan, Zachary

AU - Matheja, Christoph

AU - Müller, Peter

AU - Poli, Federico

AU - Summers, Alexander J.

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - Deductive verification

KW - Rust

KW - Separation logic

U2 - 10.1007/978-3-031-06773-0_5

DO - 10.1007/978-3-031-06773-0_5

M3 - Article in proceedings

AN - SCOPUS:85131149761

SN - 9783031067723

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 88

EP - 108

BT - NASA Formal Methods

A2 - Deshmukh, Jyotirmoy V.

A2 - Havelund, Klaus

A2 - Perez, Ivan

PB - Springer

Y2 - 24 May 2022 through 27 May 2022

ER -

Astrauskas V, Bílý A, Fiala J, Grannan Z, Matheja C, Müller P et al. The Prusti Project: Formal Verification for Rust. In Deshmukh JV, Havelund K, Perez I, editors, NASA Formal Methods . Springer. 2022. p. 88-108. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13260 LNCS). doi: 10.1007/978-3-031-06773-0_5