Скачать или смотреть [PLDI'25] A Hybrid Approach to Semi-automated Rust Verification

A Hybrid Approach to Semi-automated Rust Verification (Video, PLDI 2025)
Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner
(Imperial College London, UK; ETH Zurich, Switzerland; Nethermind, UK / Imperial College London, UK; Imperial College London, UK)

Abstract: We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verification of unsafe Rust.
To this end, we present Gillian-Rust, a proof-of-concept semi-automated verification tool built on top of the Gillian platform that can reason about type safety and functional correctness of unsafe code. Gillian-Rust automates a rich separation logic for real-world Rust, embedding the lifetime logic of RustBelt and the parametric prophecies of RustHornBelt, and is able to verify real-world Rust standard library code with only minor annotations and with verification times orders of magnitude faster than those of comparable tools.
We link Gillian-Rust with Creusot, a state-of-the-art verifier for safe Rust, by providing a systematic encoding of unsafe code specifications that Creusot can use but cannot verify, demonstrating the feasibility of our hybrid approach.

Article: https://doi.org/10.1145/3729289

Supplementary archive: https://doi.org/10.5281/zenodo.15183201 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)

ORCID: https://orcid.org/0000-0001-9419-5387, https://orcid.org/0000-0003-2530-8418, https://orcid.org/0000-0002-0400-7467, https://orcid.org/0000-0002-4187-0585

Video Tags: Rust, semi-automatic verification, symbolic execution, compositionality, pldi25main-p198-p, doi:10.1145/3729289, doi:10.5281/zenodo.15183201, orcid:0000-0001-9419-5387, orcid:0000-0003-2530-8418, orcid:0000-0002-0400-7467, orcid:0000-0002-4187-0585, Artifacts Available, Artifacts Evaluated — Reusable

Presentation at the PLDI 2025 conference, June 16–20, 2025, https://pldi25.sigplan.org/
Sponsored by ACM SIGPLAN,