Publications related to Creusot

2026

Boucler la boucle du parcours de Morris

by Arnaud Golfouse, Paul Patault in JFLA 2026
[Paper] [Artifact]

Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust

by Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan in CPP 2026
[Paper]

2025

A Hybrid Approach to Semi-automated Rust Verification

by Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, Philippa Gardner in PLDI 2025
[Paper]

Coma, an Intermediate Verification Language with Explicit Abstraction Barriers

by Andrei Paskevitch, Paul Patault, Jean-Christophe Filliâtre in ESOP 2025
[Paper]

Remonter les barrières pour ouvrir une clôture

by Paul Patault, Arnaud Golfouse, Xavier Denis in JFLA 2025
[Paper]

Using a Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool

by Xavier Denis, Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan, Dominik Stolz
[Draft]

2023

Deductive verification of Rust programs

by Xavier Denis
[Thesis]

Specifying and Verifying Higher-order Rust Iterators

by Xavier Denis, Jacques-Henri Jourdan in ETAPS 2023
[Paper]

2022

Creusot: a Foundry for the Deductive Verification of Rust Programs

by Xavier Denis, Jacques-Henri Jourdan, Claude Marché in ICFEM 2022
[Paper]

CreuSAT: Using Rust and Creusot to create the world's fastest deductively verified SAT solver

by Sarek Høverstad Skotåm
[Master's thesis] [Code]

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code

by Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer in PLDI 2022
[Paper] [Artifact]

2021

RustHorn: CHC-based Verification for Rust Programs

by Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi in TOPLAS 2021
[Paper]