Jacques-Henri Jourdan

According to our database1, Jacques-Henri Jourdan authored at least 21 papers between 2012 and 2020.

Collaborative distances:



In proceedings 
PhD thesis 


On csauthors.net:


Spy game: verifying a local generic solver in Iris.
Proc. ACM Program. Lang., 2020

Cosmo: a concurrent separation logic for multicore OCaml.
Proc. ACM Program. Lang., 2020

RustBelt meets relaxed memory.
Proc. ACM Program. Lang., 2020

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Time Credits and Time Receipts in Iris.
Proceedings of the Programming Languages and Systems, 2019

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang., 2018

RustBelt: securing the foundations of the rust programming language.
Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program., 2018

A Simple, Possibly Correct LR Parser for C11.
ACM Trans. Program. Lang. Syst., 2017

Sparsity Preserving Algorithms for Octagons.
Electron. Notes Theor. Comput. Sci., 2017

The Essence of Higher-Order Concurrent Separation Logic.
Proceedings of the Programming Languages and Systems, 2017

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

dfcomb: An R-package for phase I/II trials of drug combinations.
Comput. Methods Programs Biomed., 2016

Verified Compilation of Floating-Point Computations.
J. Autom. Reason., 2015

A Formally-Verified C Static Analyzer.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Implementing and Reasoning About Hash-consed Data Structures in Coq.
J. Autom. Reason., 2014

Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials.
Proceedings of the American Control Conference, 2014

Implementing Hash-Consed Structures in Coq.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.
Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

3D Hardware Canaries.
IACR Cryptol. ePrint Arch., 2012

Validating LR(1) Parsers.
Proceedings of the Programming Languages and Systems, 2012