A Refinement Methodology for Distributed Programs in Rust
OPEN ACCESS
Loading...
Author / Producer
Date
2025
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Refinement relates an abstract system model to a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Top-down refinement techniques that automatically generate executable code generally produce implementations with sub-optimal performance. Bottom-up refinement allows one to reason about existing, efficient implementations, but imposes strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools.
In this paper, we present a novel bottom-up refinement methodology that removes these limitations. Our methodology uses the familiar notion of guarded transition systems to express abstract models, but combines guards with a novel notion of \emph{locally-inductive invariants} to relate the abstract model \emph{locally} to concrete state. This approach is much more flexible than standard coupling invariants; in particular, it supports a wide range of program structures, data representations, and proof structures. We integrate our methodology as a library into Rust, leveraging the Rust type system to reason about ownership of guards. This integration allows one to use our methodology with an off-the-shelf Rust verification tool. It also facilitates practical applications, as we demonstrate on a number of substantial case studies including a concurrent implementation of Memcached.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
9 (OOPSLA2)
Pages / Article No.
341
Publisher
Association for Computing Machinery
Event
OOPSLA SPLASH 2025
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Conference lecture on October 18, 2025.