Jacques-Henri Jourdan

ORCID

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 19

Top Venues

Proc. ACM Program. Lang.

J. Autom. Reason.

ESOP

ITP

Paris Diderot University, France (PHD)

Education History

Paris Diderot University, France

PHD

Publications

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

Jacques-Henri Jourdan.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Jacques-Henri Jourdan