3D Hardware Canaries. - Sébastien Briais; Stéphane Caron; Jean-Michel Cioranesco; Jean-Luc Danger; Sylvain Guilley; Jacques-Henri Jourdan; Arthur Milchior; David Naccache; Thibault Porteboeuf (CHES, 2012)

Validating LR(1) Parsers. - Jacques-Henri Jourdan; François Pottier; Xavier Leroy (ESOP, 2012)

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2013)

Implementing Hash-Consed Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (ITP, 2013)

Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials. - Eric Goubault; Jacques-Henri Jourdan; Sylvie Putot; Sriram Sankaranarayanan 001 (ACC, 2014)

Implementing and Reasoning About Hash-consed Data Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (J. Autom. Reason., 2014)

A Formally-Verified C Static Analyzer. - Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie (POPL, 2015)

Verified Compilation of Floating-Point Computations. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (J. Autom. Reason., 2015)

dfcomb: An R-package for phase I/II trials of drug combinations. - Marie-Karelle Riviere; Jacques-Henri Jourdan; Sarah Zohar (Comput. Methods Programs Biomed., 2016)

Sparsity Preserving Algorithms for Octagons. - Jacques-Henri Jourdan (NSAD@SAS, 2016)

Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement vérifié). - Jacques-Henri Jourdan (2016)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

A Simple, Possibly Correct LR Parser for C11. - Jacques-Henri Jourdan; François Pottier (ACM Trans. Program. Lang. Syst., 2017)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

RustBelt: securing the foundations of the rust programming language. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Time Credits and Time Receipts in Iris. - Glen Mével; Jacques-Henri Jourdan; François Pottier (ESOP, 2019)

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. - Armaël Guéneau; Jacques-Henri Jourdan; Arthur Charguéraud; François Pottier (ITP, 2019)

RustBelt meets relaxed memory. - Hoang-Hai Dang; Jacques-Henri Jourdan; Jan-Oliver Kaiser; Derek Dreyer (Proc. ACM Program. Lang., 2020)

Cosmo: a concurrent separation logic for multicore OCaml. - Glen Mével; Jacques-Henri Jourdan; François Pottier (Proc. ACM Program. Lang., 2020)

Spy game: verifying a local generic solver in Iris. - Paulo Emílio de Vilhena; François Pottier; Jacques-Henri Jourdan (Proc. ACM Program. Lang., 2020)

Safe systems programming in Rust. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Commun. ACM, 2021)

Formal verification of a concurrent bounded queue in a weak memory model. - Glen Mével; Jacques-Henri Jourdan (Proc. ACM Program. Lang., 2021)

Creusot: A Foundry for the Deductive Verification of Rust Programs. - Xavier Denis; Jacques-Henri Jourdan; Claude Marché (ICFEM, 2022)

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. - Yusuke Matsushita 002; Xavier Denis; Jacques-Henri Jourdan; Derek Dreyer (PLDI, 2022)

Specifying and Verifying Higher-order Rust Iterators. - Xavier Denis; Jacques-Henri Jourdan (TACAS (2), 2023)

Thunks and Debits in Separation Logic with Time Credits. - François Pottier; Armaël Guéneau; Jacques-Henri Jourdan; Glen Mével (Proc. ACM Program. Lang., 2024)