| 2026 | IJCAR | Pgeon: Generating Tableau-Based Provers from Declarative Specifications of Logical Calculi. | Romain Sidhoum, Simon Robillard, David Delahaye |
| 2022 | CADE | Goland: A Concurrent Tableau-Based Theorem Prover (System Description). | Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane |
| 2019 | ICCS | Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms. | Jessie Carbonnel, David Delahaye, Marianne Huchard, Clmentine Nebut |
| 2018 | SEKE | Recovering Three-Level Architectures from the Code of Open-Source Java Spring Projects (S). | Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier |
| 2017 | SEKE | Substitutability-Based Version Propagation to Manage the Evolution of Three-Level Component-Based Architectures. | Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier |
| 2015 | LPAR | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. | Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant |
| 2015 | TABLEAUX | Integrating Simplex with Tableaux. | Guillaume Bury, David Delahaye |
| 2013 | LPAR | Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. | David Delahaye, Damien Doligez, Frdric Gilbert, Pierre Halmagrand, Olivier Hermant |
| 2012 | CADE | Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. | Mlanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
| 2012 | CPP | Producing Certified Functional Code from Inductive Specifications. | Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois |
| 2011 | SEFM | Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. | Mlanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
| 2008 | RE | Formal Modeling of Airport Security Regulations using the Focal Environment. | David Delahaye, Jean-Frdric tienne, Vronique Donzeau-Gouge |
| 2008 | TASE | Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. | David Delahaye, Jean-Frdric tienne, Vronique Donzeau-Gouge |
| 2007 | LPAR | Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. | Richard Bonichon, David Delahaye, Damien Doligez |
| 2006 | CaiSE | Modeling Airport Security Regulations in Focal. | David Delahaye, Jean-Frdric tienne, Vronique Donzeau-Gouge |
| 2006 | FM | Certifying Airport Security Regulations Using the Focal Environment. | David Delahaye, Jean-Frdric tienne, Vronique Donzeau-Gouge |
| 2006 | ISoLA | Reasoning about Airport Security Regulations Using the Focal Environment. | David Delahaye, Jean-Frdric tienne, Vronique Donzeau-Gouge |
| 2000 | LPAR | A Tactic Language for the System Coq. | David Delahaye |