Jacques-Henri Jourdan
Jacques-Henri Jourdan
CNRS, LRI, Univ. Paris-Sud, Université Paris Saclay
Verified email at normalesup.org - Homepage
TitleCited byYear
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
1232015
Validating LR (1) Parsers
JH Jourdan, F Pottier, X Leroy
22nd European Symposium on Programming (ESOP 2012), 224-243, 2012
722012
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
632018
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
632017
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
482013
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
362018
Verified Compilation of Floating-Point Computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54 (2), 135-163, 2015
332015
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
262012
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
212014
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
172018
Verasco: a Formally Verified C Static Analyzer
JH Jourdan
Université Paris Diderot (Paris 7), 2016
162016
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
82018
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
72014
Implementing hash-consed structures in Coq
T Braibant, JH Jourdan, D Monniaux
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes …, 2013
52013
Sparsity Preserving Algorithms for Octagons
JH Jourdan
Numerical and Symbolic Abstract Domains, 2016
42016
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
32019
Time credits and time receipts in Iris
G Mével, JH Jourdan, F Pottier
European Symposium on Programming, 3-29, 2019
32019
RustBelt Relaxed
HH Dang, JH Jourdan, JO Kaiser, D Dreyer
Submitted for publication, 2018
22018
A simple, possibly correct LR parser for C11
JH Jourdan, F Pottier
ACM Transactions on Programming Languages and Systems (TOPLAS) 39 (4), 14, 2017
22017
dfcomb: An R-package for phase I/II trials of drug combinations
MK Riviere, JH Jourdan, S Zohar
Computer methods and programs in biomedicine 125, 117-133, 2016
12016
The system can't perform the operation now. Try again later.
Articles 1–20