Jacques-Henri Jourdan

According to our database, Jacques-Henri Jourdan authored at least 27 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

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., January, 2024

2023

Specifying and Verifying Higher-order Rust Iterators.

Xavier Denis, Jacques-Henri Jourdan

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022

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

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Creusot: A Foundry for the Deductive Verification of Rust Programs.

Xavier Denis, Jacques-Henri Jourdan, Claude Marché

Proceedings of the Formal Methods and Software Engineering, 2022

2021

Formal verification of a concurrent bounded queue in a weak memory model.

Glen Mével, Jacques-Henri Jourdan

Proc. ACM Program. Lang., 2021

Safe systems programming in Rust.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Commun. ACM, 2021

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

Cosmo: a concurrent separation logic for multicore OCaml.

Glen Mével, Jacques-Henri Jourdan, François Pottier

Proc. ACM Program. Lang., 2020

RustBelt meets relaxed memory.

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer

Proc. ACM Program. Lang., 2020

2019

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Time Credits and Time Receipts in Iris.

Glen Mével, Jacques-Henri Jourdan, François Pottier

Proceedings of the Programming Languages and Systems, 2019

2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer

Proc. ACM Program. Lang., 2018

RustBelt: securing the foundations of the rust programming language.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer

J. Funct. Program., 2018

2017

A Simple, Possibly Correct LR Parser for C11.

Jacques-Henri Jourdan, François Pottier

ACM Trans. Program. Lang. Syst., 2017

The Essence of Higher-Order Concurrent Separation Logic.

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2017

2016

Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement vérifié).

Jacques-Henri Jourdan

PhD thesis, 2016

Sparsity Preserving Algorithms for Octagons.

Jacques-Henri Jourdan

Proceedings of the Sixth Workshop on Numerical and Symbolic Abstract Domains, 2016

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

2015

Verified Compilation of Floating-Point Computations.

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond

J. Autom. Reason., 2015

A Formally-Verified C Static Analyzer.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Implementing and Reasoning About Hash-consed Data Structures in Coq.

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

J. Autom. Reason., 2014

Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials.

Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan

Proceedings of the American Control Conference, 2014

2013

Implementing Hash-Consed Structures in Coq.

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond

Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

2012

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

IACR Cryptol. ePrint Arch., 2012

Validating LR(1) Parsers.

Jacques-Henri Jourdan, François Pottier, Xavier Leroy

Proceedings of the Programming Languages and Systems, 2012