POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

As Rust’s popularity increases, the need for ensuring correctness properties of software written in Rust also increases. In recent years, much work has been done to develop tools to analyze Rust programs, including Property-Based Testing (PBT), model checking, and verification tools. However, developers still need to specify the properties that need to be analyzed and write test harnesses to perform the analysis. We observe that one kind of correctness properties that has been overlooked is correctness invariants of Rust trait implementations; for instance, implementations of the equality trait need to be reflexive, symmetric, and transitive. In this paper, we develop a fully automated tool that allows developers to analyze their implementations of a set of built-in Rust traits. We encoded the test harnesses for the correctness properties of these traits and use Kani to verify them. We evaluated our tool over six open-source Rust libraries and identified three issues in PROST!, a protocol buffer library with nearly 40 million downloads.

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Session 5: keynote, Program and System VerificationVMCAI at Marconi Room
Chair(s): Ori Lahav Tel Aviv University
Automating Relational Verification of Infinite-State Programs
Hiroshi Unno University of Tsukuba
Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Philip Tasche University of Twente, Raúl E. Monti University of Twente, Stefanie Eva Drerup University of Münster, Pauline Blohm Uni Münster, Paula Herber University of Munster, Germany, Marieke Huisman University of Twente
Automatically Enforcing Rust Trait Properties
Twain Byrnes Carnegie Mellon University, Yoshiki Takashima Carnegie Mellon University, Limin Jia Carnegie Mellon University