Jacques-Henri Jourdan
YOU?
Author Swipe
View article: Using a Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool
Using a Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool Open
Verification tools targeting Rust programs need to handle a salient feature of this language: mutable borrows. The elegant approach of using prophecies to model mutable borrows is used in practice in the Creusot deductive verification tool…
View article: Thunks and Debits in Separation Logic with Time Credits
Thunks and Debits in Separation Logic with Time Credits Open
A thunk is a mutable data structure that offers a simple memoization service: it stores either a suspended computation or the result of this computation. Okasaki [1999] presents many data structures that exploit thunks to achieve good amor…
View article: RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code Open
International audience
View article: Formal verification of a concurrent bounded queue in a weak memory model
Formal verification of a concurrent bounded queue in a weak memory model Open
We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as …
View article: Safe systems programming in Rust
Safe systems programming in Rust Open
The promise and the challenges of the first industry-supported language to master the trade-off between safety and control.
View article: The Creusot Environment for the Deductive Verification of Rust Programs
The Creusot Environment for the Deductive Verification of Rust Programs Open
Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification of Rust code, which aims a…
View article: Cosmo: a concurrent separation logic for multicore OCaml
Cosmo: a concurrent separation logic for multicore OCaml Open
Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while …
View article: Safe Systems Programming in Rust: The Promise and the Challenge
Safe Systems Programming in Rust: The Promise and the Challenge Open
International audience
View article: RustBelt meets relaxed memory
RustBelt meets relaxed memory Open
The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust’s safety claims on a more rigorous formal foun…
View article: Spy game: verifying a local generic solver in Iris
Spy game: verifying a local generic solver in Iris Open
We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. T…
View article: Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm Open
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with …
View article: MoSeL: a general, extensible modal framework for interactive proofs in separation logic
MoSeL: a general, extensible modal framework for interactive proofs in separation logic Open
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics …
View article: Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Iris from the ground up: A modular foundation for higher-order concurrent separation logic Open
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of si…
View article: RustBelt: securing the foundations of the Rust programming language
RustBelt: securing the foundations of the Rust programming language Open
Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have b…
View article: RustBelt: Securing the Foundations of the Rust Programming Language -- Artifact
RustBelt: Securing the Foundations of the Rust Programming Language -- Artifact Open
This is the artifact accompanying the POPL18 paper "RustBelt: Securing the Foundations of the Rust Programming Language". You can find the latest version of this artifact online at https://gitlab.mpi-sws.org/FP/LambdaRust-coq. This archive…
View article: A Simple, Possibly Correct LR Parser for C11
A Simple, Possibly Correct LR Parser for C11 Open
The syntax of the C programming language is described in the C11 standard by an ambiguous context-free grammar, accompanied with English prose that describes the concept of “scope” and indicates how certain ambiguous code fragments should …
View article: Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization
Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization Open
Conventionally, phase I dose-finding trials aim to determine the maximum tolerated dose of a new drug under the assumption that both toxicity and efficacy monotonically increase with the dose. This paradigm, however, is not suitable for so…
View article: Statistically Profiling Memory in OCaml
Statistically Profiling Memory in OCaml Open
International audience