See also my google scholar and dblp pages.

[1]

François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével. Thunks and debits in separation logic with time credits. In Symposium on Principles of Programming Languages (POPL). ACM, January 2024. [ bib | DOI | .pdf | Abstract ]

[2]

Xavier Denis and Jacques-Henri Jourdan. Specifying and verifying higher-order rust iterators. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer Verlag, April 2023. [ bib | DOI | .pdf | Abstract ]

[3]

Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: a foundry for the deductive verication of rust programs. In International Conference on Formal Engineering Methods (ICFEM). Springer Verlag, October 2022. [ bib | DOI | .pdf | Abstract ]

[4]

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. RustHornBelt: A semantic foundation for functional verification of rust programs with unsafe code. In Conference on Programming Language Design and Implementation (PLDI). ACM, June 2022. [ bib | DOI | .pdf | Abstract ]

[5]

Glen Mével and Jacques-Henri Jourdan. Formal verification of a concurrent bounded queue in a weak memory model. In International Conference on Functional Programming (ICFP). ACM, September 2021. [ bib | DOI | .pdf | Abstract ]

[6]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Safe systems programming in Rust: The promise and the challenge. Communications of The ACM, 64(4):144–152, March 2021. [ bib | DOI | .pdf | Abstract ]

[7]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. Cosmo: A concurrent separation logic for Multicore OCaml. In International Conference on Functional Programming (ICFP). ACM, September 2020. [ bib | DOI | .pdf | Abstract ]

[8]

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Dreyer Derek. RustBelt meets relaxed memory. In Symposium on Principles of Programming Languages (POPL). ACM, January 2020. [ bib | DOI | .pdf | Abstract ]

[9]

Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan. Spy game: Verifying a local generic solver in Iris. In Symposium on Principles of Programming Languages (POPL). ACM, January 2020. [ bib | DOI | .pdf | Abstract ]

[10]

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and Pottier François. Formal proof and analysis of an incremental cycle detection algorithm. In Interactive Theorem Proving (ITP), September 2019. [ bib | DOI | .pdf | Abstract ]

[11]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In European Symposium on Programming (ESOP). Springer, April 2019. [ bib | DOI | .pdf | Abstract ]

[12]

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. In International Conference on Functional Programming (ICFP). ACM, September 2018. [ bib | DOI | .pdf | Abstract ]

[13]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up. Journal of Functional Programming (JFP), 28(e20), 2018. [ bib | DOI | .pdf | Abstract ]

[14]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. In Symposium on Principles of Programming Languages (POPL). ACM, January 2018. [ bib | DOI | .pdf | Abstract ]

[15]

Jacques-Henri Jourdan and François Pottier. A simple, possibly correct LR parser for C11. Transactions on Programming Languages and Systems (TOPLAS), 39(4), August 2017. [ bib | DOI | .pdf | Abstract ]

[16]

Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher-order concurrent separation logic. In European Symposium on Programming (ESOP). Springer, April 2017. [ bib | DOI | .pdf | Abstract ]

[17]

Jacques-Henri Jourdan. Sparsity preserving algorithms for octagons. In Numerical and Symbolic Abstract Domains Workshop (NSAD), pages 57–70. Elsevier, September 2016. [ bib | DOI | .pdf | Abstract ]

[18]

Jacques-Henri Jourdan. Statistically profiling memory in OCaml. OCaml Workshop, September 2016. [ bib | .pdf ]

[19]

Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. PhD thesis, Université Paris Diderot (Paris 7), May 2016. [ bib | .pdf | Abstract ]

[20]

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning (JAR), 54(2):135–163, February 2015. [ bib | DOI | .pdf | Abstract ]

[21]

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In Symposium on Principles of Programming Languages (POPL), pages 247–259. ACM, January 2015. [ bib | DOI | .pdf | Abstract ]

[22]

Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing and reasoning about hash-consed data structures in Coq. Journal of Automated Reasoning (JAR), 53(3):271–304, October 2014. [ bib | DOI | .pdf | Abstract ]

[23]

Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, and Sriram Sankaranarayanan. Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through darboux polynomials. In American Control Conference (ACC), pages 3571–3578. IEEE, June 2014. [ bib | DOI | .pdf | Abstract ]

[24]

Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. In Interactive Theorem Proving (ITP), pages 477–483, July 2013. [ bib | DOI | .pdf | Abstract ]

[25]

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In IEEE Symposium on Computer Arithmetic (ARITH), pages 107–115. IEEE, April 2013. [ bib | DOI | .pdf | Abstract ]

[26]

Sébastien Briais, Stéphane Caron, Jean-Michel Cioranesco, Jean-Luc Danger, Sylvain Guilley, Jacques-Henri Jourdan, Arthur Milchior, David Naccache, and Thibault Porteboeuf. 3D hardware canaries. In Cryptographic Hardware and Embedded Systems (CHES), pages 1–22. Springer, September 2012. [ bib | DOI | .pdf | Abstract ]

[27]

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In European Symposium on Programming (ESOP), pages 397–416. Springer, March 2012. [ bib | DOI | .pdf | Abstract ]

This file was generated by bibtex2html 1.99.