Jacques-Henri Jourdan

32 papers A* 2A 4B 3C 3Journal 17Unranked 2
YearRankTypeTitle / Venue / Authors
2026 B conf
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust.
CPP
Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan
2024 J jnl
Thunks and Debits in Separation Logic with Time Credits.
Proc. ACM Program. Lang.
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
2023 — conf
Specifying and Verifying Higher-order Rust Iterators.
TACAS (2)
Xavier Denis, Jacques-Henri Jourdan
2022 C conf
Creusot: A Foundry for the Deductive Verification of Rust Programs.
ICFEM
Xavier Denis, Jacques-Henri Jourdan, Claude Marché
2022 A* conf
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code.
PLDI
Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer
2021 J jnl
Formal verification of a concurrent bounded queue in a weak memory model.
Proc. ACM Program. Lang.
Glen Mével, Jacques-Henri Jourdan
2021 J jnl
Safe systems programming in Rust.
Commun. ACM
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2020 J jnl
Cosmo: a concurrent separation logic for multicore OCaml.
Proc. ACM Program. Lang.
Glen Mével, Jacques-Henri Jourdan, François Pottier
2020 J jnl
RustBelt meets relaxed memory.
Proc. ACM Program. Lang.
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer
2020 J jnl
Spy game: verifying a local generic solver in Iris.
Proc. ACM Program. Lang.
Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
2019 B conf
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.
ITP
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
2019 A conf
Time Credits and Time Receipts in Iris.
ESOP
Glen Mével, Jacques-Henri Jourdan, François Pottier
2018 J jnl
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018 J jnl
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang.
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018 J jnl
RustBelt: securing the foundations of the rust programming language.
Proc. ACM Program. Lang.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017 J jnl
A Simple, Possibly Correct LR Parser for C11.
ACM Trans. Program. Lang. Syst.
Jacques-Henri Jourdan, François Pottier
2017 A conf
The Essence of Higher-Order Concurrent Separation Logic.
ESOP
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2016 J jnl
Sparsity Preserving Algorithms for Octagons.
CoRR
Jacques-Henri Jourdan
2016 — conf
Sparsity Preserving Algorithms for Octagons.
NSAD@SAS
Jacques-Henri Jourdan
2016 — —
Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement vérifié).
Jacques-Henri Jourdan
2016 J jnl
dfcomb: An R-package for phase I/II trials of drug combinations.
Comput. Methods Programs Biomed.
Marie-Karelle Riviere, Jacques-Henri Jourdan, Sarah Zohar
2015 A* conf
A Formally-Verified C Static Analyzer.
POPL
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
2015 J jnl
Verified Compilation of Floating-Point Computations.
J. Autom. Reason.
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2014 C conf
Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials.
ACC
Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan
2014 J jnl
Implementing and Reasoning About Hash-consed Data Structures in Coq.
J. Autom. Reason.
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 C conf
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.
IEEE Symposium on Computer Arithmetic
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2013 B conf
Implementing Hash-Consed Structures in Coq.
ITP
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing and reasoning about hash-consed data structures in Coq.
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing hash-consed structures in Coq
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2012 A conf
3D Hardware Canaries.
CHES
Sébastien Briais, Stéphane Caron, Jean-Michel Cioranesco, Jean-Luc Danger, Sylvain Guilley, Jacques-Henri Jourdan, Arthur Milchior, David Naccache, Thibault Porteboeuf
2012 J jnl
3D Hardware Canaries.
IACR Cryptol. ePrint Arch.
Sébastien Briais, Stéphane Caron, Jean-Michel Cioranesco, Jean-Luc Danger, Sylvain Guilley, Jacques-Henri Jourdan, Arthur Milchior, David Naccache, Thibault Porteboeuf
2012 A conf
Validating LR(1) Parsers.
ESOP
Jacques-Henri Jourdan, François Pottier, Xavier Leroy