|
 
|
David Delahaye
|
Equipe SYS Parti depuis le 01/09/2015 Mail : david.delahaye  cnam.fr
Tel : 0158808733 Fax : 0140272709 http://cedric.cnam.fr/~delahaye/ |
David's Tag-Cloud :
automated theorem proving,
b method,
constraint solver,
coq,
deduction modulo,
extraction,
first order prover,
inductive type,
logical framework,
programming language,
proof checking,
proof compression,
proof obligation,
proof verification,
prover,
rewriting,
smt solver,
set,
set theory,
superdeduction,
tableaux,
zenon
|
Projets
Publications
2014
- [DDM14] D. Delahaye, C. Dubois, C. Marché, D. Mentré. "The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations", Abstract State Machines, Alloy, B, VDM, and Z (ABZ), June 2014, pp.-,
- [DD14] D. Delahaye, C. Dubois. "Proceedings of the first workshop about Sets and Tools, SETS 2014, affiliated to ABZ 2014", June 2014, Informal proceedings,
Conférence Internationale avec comité de lecture
Directions d'ouvrages scientifiques
2013
- [JBD13] M. Jacquel, K. Berkani, D. Delahaye, C. Dubois. "Verifying B proof rules using deep embedding and automated theorem proving", Software & Systems Modeling (SoSym), pp. online, 2013, (doi:10.1007/s10270-013-0322-z)
- [DJ13] D. Delahaye, M. Jacquel. "Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction", Electronic Journal of Mathematics and Technology (eJMT), vol. 7(2), pp. online, 2013
- [DDG13] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant. "Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo", Logic for Programming Artificial Intelligence and Reasoning (LPAR), December 2013, Vol. 8312, pp.274-290, Series LNCS/ARCoSS, Stellenbosch, South Africa,
- [DDG13a] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant. "Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps", International Workshop on the Implementation of Logics, December 2013, pp.-,
- [DDT13] D. Delahaye, C. Dubois, P. Tollitte. "RelExt : Synthèse de code à partir de spécifications inductives ", AFADL 2013, April 2013, pp.4 pages, Nancy, France,
- [Del13] D. Delahaye. "Automated Deduction Modulo", Proof-Search in Axiomatic Theories and Type Theories (PSATTT), November 2013, pp.online, Palaiseau, France,
Revue Internationale avec comité de lecture
Conférence Internationale avec comité de lecture
Conférence Nationale avec comité de lecture
Conférences invitées
2012
- [TDD12] P. Tollitte, D. Delahaye, C. Dubois. "Producing Certified Functional Code from Inductive Specifications", International Conference on Certified Programs and Proofs (CPP 2012), December 2012, Vol. 7679, pp.76-91, Series LNCS, Kyoto, Japan,
- [JBD12] M. Jacquel, K. Berkani, D. Delahaye, C. Dubois. "Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover", International Joint Conference on Automated Reasoning (IJCAR 2012), June 2012, Vol. 7364, pp.332--338, Series LNAI, Manchester, UK,
- [BDD12] K. Berkani, D. Delahaye, C. Dubois, M. Jacquel, M. Keogh, E. Le Lay. "BCARe : un environnement pour la vérification de règles de l’Atelier B ", Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2012), January 2012, pp.46-49, Grenoble, France,
Conférence Internationale avec comité de lecture
Conférence Nationale avec comité de lecture
2011
- [JBD11] M. Jacquel, K. Berkani, D. Delahaye, C. Dubois. "Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving.", Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, November 2011, Vol. 7041, pp.253-268, Series LNCS, Montevideo, Uruguay,
Conférence Internationale avec comité de lecture
2010
- [DDT10] D. Delahaye, C. Dubois, P. Tollitte. "Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize", Journées Francophones des Langages Applicatifs (JFLA'10), January 2010, pp.55-81, Series Studia informatica universalis , La Ciotat ,
- [DRA10] D. Delahaye, R. Rioboo, S. Autexier, J. Calmet, P. Ion, L. Rideau, A. Sexton. "Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings", July 2010, Springer,
- [Del10] D. Delahaye. "Assisting Users of Proof Assistants", Soutenue le: 09 December 2010,
Conférence Nationale avec comité de lecture
Directions d'ouvrages scientifiques
Mémoire de HDR
2008
- [DEV08a] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "Producing UML Models from Focal Specifications: An Application to Airport Security Regulations", TASE'08 Theoretical Aspects of Software Engineering, Nanjing (China), January 2008, pp.121-124,
- [DEV08b] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "Formal Modeling of Airport Security Regulations using the Focal Environment", RELAW'08 Requirements Engineering and Law, Barcelona (Spain), January 2008, pp.16-20,
- [DEV08] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations", UML&FM'08 UML and Formal Methods, Kitakyushu-City (Japan), January 2008, Vol. 4, pp.267-274, Series ISSE,
- [ACD08] P. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, T. Hardin, M. Jaume, C. Morisset, F. Pessaux, P. Weis. "Trusted Software within FoCaL", CE&SAR 2008, Rennes, décembre, December 2008, pp.142-157,
Conférence Internationale avec comité de lecture
Conférence Nationale avec comité de lecture
2007
- [DDE07] D. Delahaye, C. Dubois, J. Etienne. "Extracting Purely Functional Contents from Logical Inductive Types", TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), January 2007, Vol. 4732, pp.70-85, Series LNCS,
- [BDD07] R. Bonichon, D. Delahaye, D. Doligez. "Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs", LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia), January 2007, pp.151-165, Series LNAI,
Conférence Internationale avec comité de lecture
2006
- [DEV06b] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "Modeling Airport Security Regulations in Focal", REMO2V'06 Regulations Modelling and their Validation & Verification, Luxembourg, January 2006, pp.806-812,
- [DEV06] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "Certifying Airport Security Regulations using the Focal Environment", FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, January 2006, Vol. 4085, pp.48-63, Series LNCS,
- [DEV06a] D. Delahaye, J. Etienne, V. Viguie Donzeau-Gouge. "Reasoning about Airport Security Regulations using the Focal Environment", ISoLA, Paphos (Cyprus), January 2006, pp.36-44,
Conférence Internationale avec comité de lecture
2005
- [DM05] D. Delahaye, M. Mayero. "Dealing with Algebraic Expressions over a Field in Coq using Maple", JSC, vol. 39(5), pp. 569-592, 2005
- [DJP05] D. Delahaye, M. Jaume, V. Prevosto. "Coq: un outil pour l'enseignement", TSI, Technique et Science Informatiques, vol. 24(9), pp. 1139-1160, 2005
- [DM05a] D. Delahaye, M. Mayero. "Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System", Calculemus, University of Newcastle upon Tyn (United Kingdom), January 2005, Vol. 151(1), pp.57-73, Series ENTCS,
Revue Internationale avec comité de lecture
Revue Nationale avec comité de lecture
Conférence Internationale avec comité de lecture
2002
-
[DEL02]
D. Delahaye.
"A Proof Dedicated Meta-Language",
Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark),
January 2002,
Vol. 70(2),
Series ENTCS,
-
[DEL02a]
D. Delahaye.
"Free-style Theorem Proving",
Proceedings of Theorem Proving in Higher Order Logics (TPHOLs), Hampton (VA, USA),
January 2002,
Vol. 2410,
pp.164-181,
Series LNCS,
Conférence Internationale avec comité de lecture
2001
-
[DM01]
D. Delahaye, M. Mayero.
"Field: une procédure de décision pour les nombres réels en Coq",
Journées Francophones des Langages Applicatifs (JFLA), Pontarlier (France),
January 2001,
-
[DEL01]
D. Delahaye.
"Conception de langages pour décrire les preuves et les automatisations dans les outils d'aide à la preuve: une étude dans le cadre du système Coq",
Soutenue le: 01 January 2001,
Conférence Nationale avec comité de lecture
Mémoire de Thèse
2000
-
[DEL00]
D. Delahaye.
"A Tactic Language for the System Coq",
Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island (France),
January 2000,
Vol. 1955,
pp.85-95,
Series LNCS/LNAI,
Conférence Internationale avec comité de lecture
1999
-
[DEL99]
D. Delahaye.
"Information Retrieval in a Coq Proof Library using Type Isomorphisms",
January 1999,
Vol. 1956,
pp.131-147,
Conférence Internationale avec comité de lecture
1997
-
[DDW97]
D. Delahaye, R. Di Cosmo, B. Werner.
" Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes",
PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques,
January 1997,
-
[DEL97]
D. Delahaye.
"Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes",
Date de dépot: 1997/01/01,
(Tech. Rep.: CEDRIC-97-730)
