Jacques-Henri Jourdan

32 papers A* 2A 4B 3C 3Journal 17Unranked 2

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust. CPP Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan
2024	J	`jnl`	Thunks and Debits in Separation Logic with Time Credits. Proc. ACM Program. Lang. François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
2023	—	`conf`	Specifying and Verifying Higher-order Rust Iterators. TACAS (2) Xavier Denis, Jacques-Henri Jourdan
2022	C	`conf`	Creusot: A Foundry for the Deductive Verification of Rust Programs. ICFEM Xavier Denis, Jacques-Henri Jourdan, Claude Marché
2022	A*	`conf`	RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. PLDI Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer
2021	J	`jnl`	Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang. Glen Mével, Jacques-Henri Jourdan
2021	J	`jnl`	Safe systems programming in Rust. Commun. ACM Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2020	J	`jnl`	Cosmo: a concurrent separation logic for multicore OCaml. Proc. ACM Program. Lang. Glen Mével, Jacques-Henri Jourdan, François Pottier
2020	J	`jnl`	RustBelt meets relaxed memory. Proc. ACM Program. Lang. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer
2020	J	`jnl`	Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
2019	B	`conf`	Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. ITP Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
2019	A	`conf`	Time Credits and Time Receipts in Iris. ESOP Glen Mével, Jacques-Henri Jourdan, François Pottier
2018	J	`jnl`	Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018	J	`jnl`	MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018	J	`jnl`	RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017	J	`jnl`	A Simple, Possibly Correct LR Parser for C11. ACM Trans. Program. Lang. Syst. Jacques-Henri Jourdan, François Pottier
2017	A	`conf`	The Essence of Higher-Order Concurrent Separation Logic. ESOP Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2016	J	`jnl`	Sparsity Preserving Algorithms for Octagons. CoRR Jacques-Henri Jourdan
2016	—	`conf`	Sparsity Preserving Algorithms for Octagons. NSAD@SAS Jacques-Henri Jourdan
2016	—	`—`	Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement vérifié). Jacques-Henri Jourdan
2016	J	`jnl`	dfcomb: An R-package for phase I/II trials of drug combinations. Comput. Methods Programs Biomed. Marie-Karelle Riviere, Jacques-Henri Jourdan, Sarah Zohar
2015	A*	`conf`	A Formally-Verified C Static Analyzer. POPL Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
2015	J	`jnl`	Verified Compilation of Floating-Point Computations. J. Autom. Reason. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2014	C	`conf`	Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials. ACC Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan
2014	J	`jnl`	Implementing and Reasoning About Hash-consed Data Structures in Coq. J. Autom. Reason. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013	C	`conf`	A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2013	B	`conf`	Implementing Hash-Consed Structures in Coq. ITP Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013	J	`jnl`	Implementing and reasoning about hash-consed data structures in Coq. CoRR Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013	J	`jnl`	Implementing hash-consed structures in Coq CoRR Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2012	A	`conf`	3D Hardware Canaries. CHES Sébastien Briais, Stéphane Caron, Jean-Michel Cioranesco, Jean-Luc Danger, Sylvain Guilley, Jacques-Henri Jourdan, Arthur Milchior, David Naccache, Thibault Porteboeuf
2012	J	`jnl`	3D Hardware Canaries. IACR Cryptol. ePrint Arch. Sébastien Briais, Stéphane Caron, Jean-Michel Cioranesco, Jean-Luc Danger, Sylvain Guilley, Jacques-Henri Jourdan, Arthur Milchior, David Naccache, Thibault Porteboeuf
2012	A	`conf`	Validating LR(1) Parsers. ESOP Jacques-Henri Jourdan, François Pottier, Xavier Leroy