Jacques-Henri Jourdan


CV: English - Francais


Email

jacques-henri.jourdan [at] lri [dot] fr

My PGP public key

Mail address

LRI, Bat 650
Univerité Paris Sud 11
91406 Orsay Cedex
France

Physical address

PCRI, bureau 70
Rue Noetzlin
91190 Gif-sur-Yvette
France

See also my google scholar and dblp pages.



[1]
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 ]
[2]
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 ]
[3]
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 ]
[4]
Jacques-Henri Jourdan. Statistically profiling memory in OCaml. OCaml Workshop, September 2016. [ bib | .pdf ]
[5]
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 ]
[6]
Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. PhD thesis, Universit√© Paris Diderot (Paris 7), May 2016. [ bib | .pdf | Abstract ]
[7]
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 ]
[8]
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 ]
[9]
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 ]
[10]
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 ]
[11]
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 ]
[12]
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 ]
[13]
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 ]
[14]
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.98.