PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Fri 20 Jun 2025 11:30 - 11:50 at Grand Ball Room 2 - Type Systems

We introduce \textsc{Thrust}, a new verification tool for ensuring functional correctness in \textsc{Rust}, distinguished by its strengths in \emph{automated} verification, including the synthesis of inductive invariants for loops and recursive functions. \textsc{Thrust} is built on a novel dependent refinement type system for \textsc{Rust} and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, \textsc{Thrust} also supports semi-automated verification utilizing user type annotations to complement CHC solvers in cases where automatic constraint solving is unsuccessful, as well as \emph{modular} verification at the function and subexpression levels.
\textsc{Thrust} also achieves \emph{precise} verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of \emph{prophecy} into the refinement type system: it not only enables strong updates by leveraging the aliasing XOR mutability'' guarantee provided by \textsc{Rust}'s type system, but also achieves propagation of update information to the original owner upon mutable borrow release through the use of a prophecy variable. Incorporating prophecy into a refinement type system is itself challenging and requires certain tricks, as discussed in this paper, making a theoretical contribution and paving the way for further research into prophecy-based refinement type systems. While our type system addresses the challenge, we keep it simple for extensibility, specifically by delegating the guarantee ofaliasing XOR mutability,'' and, more technically, the ``well-borrowedness'' of the program in the sense of the \emph{stacked borrows} aliasing model, to \textsc{Rust}'s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to \textsc{RustHorn}, another automated verification tool based on prophecy, our approach leverages the strengths of refinement types to support modular verification, higher-order functions, and refinement of data stored in algebraic data structures.
We implemented \textsc{Thrust}, a refinement type inference tool as a plugin for the \textsc{Rust} compiler, and evaluated it using \textsc{RustHorn} benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of \textsc{RustHorn} and other semi-automated verification tools, obtaining promising results.

This program is tentative and subject to change.

Fri 20 Jun

Displayed time zone: Seoul change

10:30 - 11:50
10:30
20m
Talk
Usability Barriers for Liquid Types
PLDI Research Papers
Catarina Gamboa Carnegie Mellon University and University of Lisbon, Abigail Elena Reese Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Jonathan Aldrich Carnegie Mellon University
DOI Pre-print
10:50
20m
Talk
Dynamic Region Ownership for Concurrency Safety
PLDI Research Papers
Fridtjof Stoldt Uppsala University, Brandt Bucher Microsoft, Sylvan Clebsch Microsoft Azure Research, Matthew A. Johnson Microsoft Azure Research, Matthew J. Parkinson Microsoft Azure Research, Guido van Rossum Microsoft, Eric Snow Microsoft, Tobias Wrigstad Uppsala University
DOI
11:10
20m
Talk
Practical Type Inference with Levels
PLDI Research Papers
Andong Fan University of Toronto, Han Xu Princeton University, Ningning Xie University of Toronto
DOI
11:30
20m
Talk
Thrust: A Prophecy-Based Refinement Type System for Rust
PLDI Research Papers
Hiromi Ogawa University of Tsukuba, Taro Sekiyama National Institute of Informatics, Hiroshi Unno Tohoku University
DOI