| 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 | 254 | 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 | 230 | 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 | 179 | 2015 |
| The Essence of Higher-Order Concurrent Separation Logic R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal ESOP, 2017 | 123 | 2017 |
| Validating LR (1) Parsers JH Jourdan, F Pottier, X Leroy 22nd European Symposium on Programming (ESOP 2012), 224-243, 2012 | 107 | 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 | 57 | 2018 |
| 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 | 56 | 2013 |
| Verified Compilation of Floating-Point Computations S Boldo, JH Jourdan, X Leroy, G Melquiond Journal of Automated Reasoning 54 (2), 135-163, 2015 | 49 | 2015 |
| 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 | 40 | 2012 |
| Safe systems programming in Rust R Jung, JH Jourdan, R Krebbers, D Dreyer Communications of the ACM 64 (4), 144-152, 2021 | 38 | 2021 |
| RustBelt meets relaxed memory HH Dang, JH Jourdan, JO Kaiser, D Dreyer Proceedings of the ACM on Programming Languages 4 (POPL), 34, 2019 | 38 | 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 | 35 | 2018 |
| Time credits and time receipts in Iris G Mével, JH Jourdan, F Pottier European Symposium on Programming, 3-29, 2019 | 31 | 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 | 29 | 2014 |
| Verasco: a Formally Verified C Static Analyzer JH Jourdan Université Paris Diderot (Paris 7), 2016 | 23 | 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 | 22 | 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 | 15 | 2014 |
| Sparsity Preserving Algorithms for Octagons JH Jourdan Numerical and Symbolic Abstract Domains, 2016 | 8 | 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 | 7 | 2017 |
| Spy game—verifying a local generic solver in Iris PE DE VILHENA, F POTTIER, JH JOURDAN | 6* | |
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org
