| 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 | 318 | 2018 |
| 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 | 310 | 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 | 200 | 2015 |
| The Essence of Higher-Order Concurrent Separation Logic R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal ESOP, 2017 | 134 | 2017 |
| Validating LR (1) Parsers JH Jourdan, F Pottier, X Leroy 22nd European Symposium on Programming (ESOP 2012), 224-243, 2012 | 115 | 2012 |
| 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 | 77 | 2018 |
| Verified compilation of floating-point computations S Boldo, JH Jourdan, X Leroy, G Melquiond Journal of Automated Reasoning 54, 135-163, 2015 | 58 | 2015 |
| 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 | 58 | 2013 |
| Safe systems programming in Rust R Jung, JH Jourdan, R Krebbers, D Dreyer Communications of the ACM 64 (4), 144-152, 2021 | 53 | 2021 |
| RustBelt meets relaxed memory HH Dang, JH Jourdan, JO Kaiser, D Dreyer Proceedings of the ACM on Programming Languages 4 (POPL), 34, 2019 | 49 | 2019 |
| 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 | 43 | 2018 |
| 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 | 43 | 2012 |
| Time credits and time receipts in Iris G Mével, JH Jourdan, F Pottier European Symposium on Programming, 3-29, 2019 | 42 | 2019 |
| 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 | 31 | 2014 |
| Formal proof and analysis of an incremental cycle detection algorithm A Guéneau, JH Jourdan, A Charguéraud, F Pottier Interactive Theorem Proving, 2019 | 27 | 2019 |
| Verasco: a Formally Verified C Static Analyzer JH Jourdan Université Paris Diderot (Paris 7), 2016 | 25 | 2016 |
| 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 | 19 | 2014 |
| 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 | 10 | 2022 |
| The Creusot Environment for the Deductive Verification of Rust Programs X Denis, JH Jourdan, C Marché Inria Saclay-Île de France, 2021 | 10 | 2021 |
| A simple, possibly correct LR parser for C11 JH Jourdan, F Pottier ACM Transactions on Programming Languages and Systems (TOPLAS) 39 (4), 14, 2017 | 9 | 2017 |
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org
