Jacques-Henri Jourdan


CV: English - Francais


Email

jacques-henri.jourdan [at] normalesup [dot] org

My PGP public key

Address (MPI-SWS)

Jacques-Henri Jourdan
Max Plank Institute for Software Systems (MPI-SWS)
Campus E1 5
D-66123 Saarbrücken
Germany

See also my google scholar and dblp pages.



[1]
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), April 2017. [ bib | .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), 2017. To appear. [ bib | .pdf | Abstract ]
[3]
Jacques-Henri Jourdan. Statistically profiling memoy in OCaml. OCaml Workshop, September 2016. [ bib | .pdf ]
[4]
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 ]
[5]
Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. PhD thesis, Université Paris Diderot (Paris 7), May 2016. [ bib | .pdf | Abstract ]
[6]
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, 2015. [ bib | DOI | .pdf | Abstract ]
[7]
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, 2015. [ bib | DOI | .pdf | Abstract ]
[8]
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, 2014. [ bib | DOI | .pdf | Abstract ]
[9]
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, 2014. [ bib | DOI | .pdf | Abstract ]
[10]
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, 2013. [ 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, 2013. [ bib | DOI | .pdf | Abstract ]
[12]
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, 2012. [ bib | DOI | .pdf | Abstract ]
[13]
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In European Symposium on Programming (ESOP), pages 397–416. Springer, 2012. [ bib | DOI | .pdf | Abstract ]

This file was generated by bibtex2html 1.98.