David Delahaye

According to our database, David Delahaye authored at least 34 papers between 1999 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory.

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard

CoRR, 2023

2022

Goéland: A Concurrent Tableau-Based Theorem Prover (System Description).

Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2020

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice.

Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant

J. Autom. Reason., 2020

Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets.

Vincent Iampietro, David Andreu, David Delahaye

Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020), 2020

2019

Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms.

Jessie Carbonnel, David Delahaye, Marianne Huchard, Clémentine Nebut

Proceedings of the Graph-Based Representation and Reasoning, 2019

2018

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

Proceedings of the 30th International Conference on Software Engineering and Knowledge Engineering, 2018

An Automation-Friendly Set Theory for the B Method.

Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018

2017

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

Proceedings of the 29th International Conference on Software Engineering and Knowledge Engineering, 2017

2015

Verifying B proof rules using deep embedding and automated theorem proving.

Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois

Softw. Syst. Model., 2015

Tableaux Modulo Theories Using Superdeduction.

Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois

CoRR, 2015

Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction.

David Delahaye, Mélanie Jacquel

CoRR, 2015

Integrating Simplex with Tableaux.

Guillaume Bury, David Delahaye

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo.

Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

2014

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations.

David Delahaye, Catherine Dubois, Claude Marché, David Mentré

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013

Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo.

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

2012

Producing Certified Functional Code from Inductive Specifications.

Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover.

Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2008

A formal and sound transformation from Focal to UML : an application to airport security regulations.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Innov. Syst. Softw. Eng., 2008

Producing UML Models from Focal Specifications: An Application to Airport Security Regulations.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Formal Modeling of Airport Security Regulations using the Focal Environment.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Proceedings of the First International Workshop on Requirements Engineering and Law, 2008

2007

Extracting Purely Functional Contents from Logical Inductive Types.

David Delahaye, Catherine Dubois, Jean-Frédéric Étienne

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.

Richard Bonichon, David Delahaye, Damien Doligez

Proceedings of the Logic for Programming, 2007

2006

Reasoning about Airport Security Regulations Using the Focal Environment.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Proceedings of the Leveraging Applications of Formal Methods, 2006

Certifying Airport Security Regulations Using the Focal Environment.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Proceedings of the FM 2006: Formal Methods, 2006

Modeling Airport Security Regulations in Focal.

David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge

Proceedings of the CAISE*06 Workshop on Regulations Modelling and their Validation and Verification ReMo2V '06, 2006

2005

Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs.

David Delahaye, Mathieu Jaume, Virgile Prevosto

Tech. Sci. Informatiques, 2005

Dealing with algebraic expressions over a field in Coq using Maple.

David Delahaye, Micaela Mayero

J. Symb. Comput., 2005

Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System.

David Delahaye, Micaela Mayero

Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2005

Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant

David Delahaye, Micaela Mayero

CoRR, 2005

2002

A Proof Dedicated Meta-Language.

David Delahaye

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

Free-Style Theorem Proving.

David Delahaye

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2001

Field, une procédure de décision pour les nombres réels en Coq.

David Delahaye, Micaela Mayero

Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001

2000

A Tactic Language for the System Coq.

David Delahaye

Proceedings of the Logic for Programming and Automated Reasoning, 2000

1999

Information Retrieval in a Coq Proof Library Using Type Isomorphisms.

David Delahaye

Proceedings of the Types for Proofs and Programs, 1999