| 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 | 127 | 2015 |
| 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 | 83 | 2018 |
| Validating LR (1) Parsers JH Jourdan, F Pottier, X Leroy 22nd European Symposium on Programming (ESOP 2012), 224-243, 2012 | 75 | 2012 |
| The Essence of Higher-Order Concurrent Separation Logic R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal ESOP, 2017 | 71 | 2017 |
| 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 | 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 | 50 | 2013 |
| Verified Compilation of Floating-Point Computations S Boldo, JH Jourdan, X Leroy, G Melquiond Journal of Automated Reasoning 54 (2), 135-163, 2015 | 37 | 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 | 28 | 2012 |
| 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 | 21 | 2014 |
| 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 | 19 | 2018 |
| Verasco: a Formally Verified C Static Analyzer JH Jourdan Université Paris Diderot (Paris 7), 2016 | 16 | 2016 |
| 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 | 12 | 2018 |
| Formal Proof and Analysis of an Incremental Cycle Detection Algorithm A Guéneau, JH Jourdan, A Charguéraud, F Pottier | 8 | 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 | 7 | 2014 |
| Implementing hash-consed structures in Coq T Braibant, JH Jourdan, D Monniaux Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes …, 2013 | 5 | 2013 |
| Time credits and time receipts in Iris G Mével, JH Jourdan, F Pottier European Symposium on Programming, 3-29, 2019 | 4 | 2019 |
| Sparsity Preserving Algorithms for Octagons JH Jourdan Numerical and Symbolic Abstract Domains, 2016 | 4 | 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 | 3 | 2017 |
| RustBelt meets relaxed memory HH Dang, JH Jourdan, JO Kaiser, D Dreyer Proceedings of the ACM on Programming Languages 4 (POPL), 34, 2019 | 2* | 2019 |
| Statistically profiling memory in OCaml JH Jourdan OCaml Workshop, 2016 | 1 | 2016 |
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org
