Jacques-Henri Jourdan

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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2020
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

2019
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

2018
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

2017
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

2016
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

2015
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

2014
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

2013
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

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

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


  Loading...