David Delahaye

Publication Activity (10 Years)

Years Active: 1999-2023
Publications (10 Years): 8

Top Topics

Automated Reasoning

Top Venues

PNSE@Petri Nets

Publications

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR (2023)
Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). IJCAR (2022)
Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. J. Autom. Reason. 64 (6) (2020)
Vincent Iampietro, David Andreu, David Delahaye
Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets. PNSE@Petri Nets (2020)
Jessie Carbonnel, David Delahaye, Marianne Huchard, Clémentine Nebut
Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms. ICCS (2019)
Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
An Automation-Friendly Set Theory for the B Method. ABZ (2018)
Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier
Recovering Three-Level Architectures from the Code of Open-Source Java Spring Projects (S). SEKE (2018)
Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier
Substitutability-Based Version Propagation to Manage the Evolution of Three-Level Component-Based Architectures. SEKE (2017)
Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. LPAR (short papers) (2015)
David Delahaye, Mélanie Jacquel
Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction. CoRR (2015)
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
Verifying B proof rules using deep embedding and automated theorem proving. Softw. Syst. Model. 14 (1) (2015)
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
Tableaux Modulo Theories Using Superdeduction. CoRR (2015)
Guillaume Bury, David Delahaye
Integrating Simplex with Tableaux. TABLEAUX (2015)
David Delahaye, Catherine Dubois, Claude Marché, David Mentré
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. ABZ (2014)
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. LPAR (2013)
Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois
Producing Certified Functional Code from Inductive Specifications. CPP (2012)
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. IJCAR (2012)
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. SEFM (2011)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. TASE (2008)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
Formal Modeling of Airport Security Regulations using the Focal Environment. RELAW (2008)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
A formal and sound transformation from Focal to UML : an application to airport security regulations. Innov. Syst. Softw. Eng. 4 (3) (2008)
David Delahaye, Catherine Dubois, Jean-Frédéric Étienne
Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs (2007)
Richard Bonichon, David Delahaye, Damien Doligez
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR (2007)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
Certifying Airport Security Regulations Using the Focal Environment. FM (2006)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
Modeling Airport Security Regulations in Focal. ReMo2V (2006)
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
Reasoning about Airport Security Regulations Using the Focal Environment. ISoLA (2006)
David Delahaye, Micaela Mayero
Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. Calculemus (2005)
David Delahaye, Micaela Mayero
Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. 39 (5) (2005)
David Delahaye, Micaela Mayero
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant CoRR (2005)
David Delahaye, Mathieu Jaume, Virgile Prevosto
Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. Tech. Sci. Informatiques 24 (9) (2005)
David Delahaye
A Proof Dedicated Meta-Language. Electron. Notes Theor. Comput. Sci. 70 (2) (2002)
David Delahaye
Free-Style Theorem Proving. TPHOLs (2002)
David Delahaye, Micaela Mayero
Field, une procédure de décision pour les nombres réels en Coq. JFLA (2001)
David Delahaye
A Tactic Language for the System Coq. LPAR (2000)
David Delahaye
Information Retrieval in a Coq Proof Library Using Type Isomorphisms. TYPES (1999)