Jacques-Henri Jourdan
Jacques-Henri Jourdan
Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur
Verified email at normalesup.org - Homepage
Cited by
Cited by
RustBelt: Securing the foundations of the Rust programming language
R Jung, JH Jourdan, R Krebbers, D Dreyer
Proceedings of the ACM on Programming Languages, 2018, 2018
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
R Jung, R Krebbers, JH Jourdan, A Bizjak, L Birkedal, D Dreyer
Journal of Functional Programming 28, 2018
A formally-verified C static analyzer
JH Jourdan, V Laporte, S Blazy, X Leroy, D Pichardie
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2015
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
Validating LR (1) Parsers
JH Jourdan, F Pottier, X Leroy
22nd European Symposium on Programming (ESOP 2012), 224-243, 2012
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
S Boldo, JH Jourdan, X Leroy, G Melquiond
IEEE Symposium on Computer Arithmetic, 107-115, 2013
Verified Compilation of Floating-Point Computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54 (2), 135-163, 2015
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
R Krebbers, JH Jourdan, R Jung, J Tassarotti, JO Kaiser, A Timany, ...
Proceedings of the ACM on Programming Languages 2 (ICFP), 77, 2018
3D hardware canaries
S Briais, S Caron, JM Cioranesco, JL Danger, S Guilley, JH Jourdan, ...
International Workshop on Cryptographic Hardware and Embedded Systems, 1-22, 2012
Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization
MK Riviere, Y Yuan, JH Jourdan, F Dubois, S Zohar
Statistical methods in medical research 27 (2), 466-479, 2018
Finding non-polynomial positive invariants and Lyapunov functions for polynomial systems through Darboux polynomials
E Goubault, JH Jourdan, S Putot, S Sankaranarayanan
2014 American Control Conference, 3571-3578, 2014
RustBelt meets relaxed memory
HH Dang, JH Jourdan, JO Kaiser, D Dreyer
Proceedings of the ACM on Programming Languages 4 (POPL), 34, 2019
Time credits and time receipts in Iris
G Mével, JH Jourdan, F Pottier
European Symposium on Programming, 3-29, 2019
Safe systems programming in Rust
R Jung, JH Jourdan, R Krebbers, D Dreyer
Communications of the ACM 64 (4), 144-152, 2021
Verasco: a Formally Verified C Static Analyzer
JH Jourdan
Université Paris Diderot (Paris 7), 2016
Formal proof and analysis of an incremental cycle detection algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
Interactive Theorem Proving, 2019
Implementing and reasoning about hash-consed data structures in Coq
T Braibant, JH Jourdan, D Monniaux
Journal of Automated Reasoning 53 (3), 271-304, 2014
Sparsity Preserving Algorithms for Octagons
JH Jourdan
Numerical and Symbolic Abstract Domains, 2016
A simple, possibly correct LR parser for C11
JH Jourdan, F Pottier
ACM Transactions on Programming Languages and Systems (TOPLAS) 39 (4), 14, 2017
Implementing hash-consed structures in Coq
T Braibant, JH Jourdan, D Monniaux
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes …, 2013
The system can't perform the operation now. Try again later.
Articles 1–20