Follow
Jacques-Henri Jourdan
Jacques-Henri Jourdan
CNRS, Laboratoire Méthodes Formelles
Verified email at normalesup.org - Homepage
Title
Cited by
Cited by
Year
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
4172018
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, e20, 2018
4152018
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
2152015
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
1582017
Validating LR (1) Parsers
JH Jourdan, F Pottier, X Leroy
22nd European Symposium on Programming (ESOP 2012), 224-243, 2012
1292012
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
942018
RustBelt meets relaxed memory
HH Dang, JH Jourdan, JO Kaiser, D Dreyer
Proceedings of the ACM on Programming Languages 4 (POPL), 34, 2019
842019
Safe systems programming in Rust
R Jung, JH Jourdan, R Krebbers, D Dreyer
Communications of the ACM 64 (4), 144-152, 2021
702021
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
622013
Verified compilation of floating-point computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54, 135-163, 2015
592015
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
522018
Time credits and time receipts in Iris
G Mével, JH Jourdan, F Pottier
European Symposium on Programming, 3-29, 2019
492019
3D hardware canaries
S Briais, S Caron, JM Cioranesco, JL Danger, S Guilley, JH Jourdan, ...
Cryptographic Hardware and Embedded Systems–CHES 2012: 14th International …, 2012
432012
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
372014
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code
Y Matsushita, X Denis, JH Jourdan, D Dreyer
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
342022
Creusot: A Foundry for the Deductive Verification of Rust Programs
X Denis, JH Jourdan, C Marché
International Conference on Formal Engineering Methods, 90-105, 2022
322022
Formal proof and analysis of an incremental cycle detection algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
Interactive Theorem Proving, 2019
302019
Verasco: a Formally Verified C Static Analyzer
JH Jourdan
Université Paris Diderot (Paris 7), 2016
262016
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
252014
Formal verification of a concurrent bounded queue in a weak memory model
G Mével, JH Jourdan
Proceedings of the ACM on Programming Languages 5 (ICFP), 1-29, 2021
162021
The system can't perform the operation now. Try again later.
Articles 1–20