Remembering Gilles Dowek
Almost one year after Gilles left us, I joined Catherine Dubois for a talk at the Tribute to Gilles Dowek, held at FLoC 2026 in Lisbon.
Tribute programme ↗
%20--%3e%3csvg%20version='1.1'%20id='Calque_1'%20xmlns='http://www.w3.org/2000/svg'%20xmlns:xlink='http://www.w3.org/1999/xlink'%20x='0px'%20y='0px'%20viewBox='0%200%2055.3%2055.3'%20style='enable-background:new%200%200%2055.3%2055.3;'%20xml:space='preserve'%3e%3cstyle%20type='text/css'%3e%20.st0{fill:%2300294B;}%20.st1{fill:%23FFFFFF;}%20%3c/style%3e%3cg%3e%3cpath%20class='st0'%20d='M26.5,0.1C26,0,25.5,0,25,0C18.2,0,12,2.9,6.6,8.7C1.6,13.9,0,18.2,0,23.3C0,26,0.5,29,1.2,32.5%20c1.3,6.6,5.3,13,10.8,17.6c4.2,3.5,8.9,5.2,13.9,5.3c2.6,0,5.2-0.4,7.9-1.4c8.6-3,16.9-11.5,20.1-20.7c1-2.9,1.5-5.8,1.5-8.5%20c0-6.6-3-12.4-8.8-16.5C39.5,3.2,32.8,0.4,26.5,0.1z'/%3e%3cg%3e%3cpath%20class='st1'%20d='M16.6,27.7h-1.9v0.1c0,0.4-0.2,3.6-3.1,3.6c-2.6,0-3.9-2.3-3.9-6.9c0-4.6,1.3-6.9,3.9-6.9%20c2.9,0,3.1,3.4,3.1,3.6v0.1h1.9c0.2,0,0.4-0.1,0.5-0.2c0.1-0.1,0.2-0.3,0.2-0.4c0-0.9-0.5-5.4-5.7-5.4c-4.2,0-6.4,3.2-6.4,9.2%20s2.2,9.2,6.4,9.2c5,0,5.6-4.1,5.7-5.3c0-0.2-0.1-0.3-0.2-0.5C17,27.8,16.8,27.7,16.6,27.7z'/%3e%3cpath%20class='st1'%20d='M46.1,23.4L46.1,23.4l-1.6-0.7c-1.6-0.7-2.1-1.4-2.1-2.6c0-1.6,1.1-2.6,2.9-2.6c1,0,1.8,0.2,2.8,1.2l0.1,0.1%20L49,18c0.5-0.5,0.4-0.9,0.1-1.2c-0.8-1-2.2-1.6-3.9-1.6c-3.1,0-5.4,2.1-5.4,4.9c0,2.8,1.7,3.9,3.6,4.8l1.7,0.7%20c1.7,0.7,2.5,1.4,2.5,3c0,2.2-2,2.8-3.2,2.8c-1,0-2.1-0.2-3.5-1.8l-0.1-0.1L40,30.4c-0.5,0.4-0.5,0.8,0,1.3%20c1.3,1.6,3.1,1.9,4.4,1.9c2.8,0,5.7-1.7,5.7-5.1C50.1,25.7,48.5,24.4,46.1,23.4z'/%3e%3cpath%20class='st1'%20d='M30,20.6c0-2.8-2.3-5.2-5.2-5.2c-1.3,0-2.6,0.5-3.5,1.3v-1h-1.7c-0.5,0-0.7,0.3-0.7,0.7V33%20c0,0.5,0.3,0.7,0.7,0.7h1.7V20.7c0-1.7,1.4-3.1,3.1-3.1c1.7,0,3.1,1.4,3.1,3.1v13.1h1.7c0.5,0,0.7-0.3,0.7-0.7%20C30,33,30,20.6,30,20.6z'/%3e%3cpath%20class='st1'%20d='M39.8,16.5c0.1-0.1,0.1-0.2,0.1-0.4c0-0.3-0.2-0.5-0.4-0.6c-0.5-0.2-1-0.2-1.6-0.2c-1.3,0-2.6,0.5-3.5,1.3v-1%20h-1.7c-0.5,0-0.7,0.3-0.7,0.7V33c0,0.5,0.3,0.7,0.7,0.7h1.7V20.6c0-1.7,1.4-3.1,3.1-3.1c0.4,0,0.9,0.1,1.3,0.3L39.8,16.5%20L39.8,16.5z'/%3e%3c/g%3e%3c/g%3e%3c/svg%3e)
Professor · Computer Science
David
Delahaye
Automated reasoning, formal methods
and proof engineering.
research.focus = ["deduction", "verification", "proof"];
FLoC 2026, LisbonMontpellier · LIRMM
Latest updates
News
Two papers at FLoC 2026
With Romain Sidhoum and Simon Robillard, we have papers accepted at IJCAR 2026 and LFMTP 2026 on Pgeon and controlled proof search.
VIP enters CASC
With Ilies Nokrani and Clémence Gérardin, we are entering VIP in the next CASC competition at FLoC 2026. Started only two months ago, the prover was written entirely through vibe coding. Results coming soon!
Explore VIP on GitHub ↗Research
Proof as a foundation for trust
My research lies at the intersection of software engineering and formal methods. Following early work on proof assistants — Coq, now Rocq, and Focalize — I now focus primarily on automated deduction in first-order logic and reasoning modulo theories.
My goal is twofold: to design efficient proof-search methods and to assess them through concrete tools and reproducible benchmarks.
Automated deduction
Concurrent tableaux, deduction modulo theory, superdeduction and proof certification.
Software dependability
Modelling and verification of critical systems, program proofs and certified compilation.
Type theory
Proof assistants, inductive relations, tactic languages and type isomorphisms.
Theories & computation
Set theory, arithmetic, geometry and interactions between deduction and computer algebra.
Software & projects
From theory to tools
Open research prototypes designed to experiment with new calculi and make results reproducible.
Active · Go
Goéland
A concurrent automated theorem prover based on first-order tableaux. “Best newcomer” award at CASC-J11 in 2022.
View repository ↗ ActivePgeon
Generation of tableau-based deduction tools from declarative specifications.
View repository ↗ Open sourceZenon Modulo
An extension of Zenon for deduction modulo theory and linear arithmetic.
View repository ↗ Open sourceArchSAT
An SMT solver combining first-order tableaux with rewriting theories.
View repository ↗ BenchmarkTarski / GeoCoq
Elementary geometry problems and machine-learning-based premise selection.
View repository ↗ ANR · National coordinatorBWare
A proof-producing platform for the automated verification of industrial B proof obligations, bringing together first-order provers and SMT solvers.
View ANR project ↗ Ongoing · ANRICSPA
Confident and interoperable proofs for B, Event-B and TLA+, independently checked through the Dedukti logical framework.
View ANR project ↗Earlier research projects
ENVIEVERTE, Quotient, SSURF, A3PAT, CerPAN (local coordinator at Cédric), ModuLogic and EDEMOI.
Interactive project · 01
ProofQuest
A game about logic, proof search and the pleasure of finding the right argument. We are developing ProofQuest as a playful way to discover formal reasoning.
In active developmentPlay ProofQuest · coming soon
PhD supervision
Learning through research
PhD supervision and co-supervision in automated reasoning, programming languages and critical systems.
Romain Sidhoum
Generating tableau-based automated deduction tools from declarative specifications of logical calculi.
Théo Laurent
Structural Subtyping in MLTT.
Julie Cailler
Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic.
Vincent Iampietro
Formal verification of a methodology for designing and producing critical digital systems.
Alexandre Le Borgne
ARIANE: Automated Re-Documentation to Improve Software Architecture Understanding and Evolution.
Guillaume Bury
Integrating Rewriting, Tableau and Superposition into SMT.
Pierre Halmagrand
Automated Deduction and Proof Certification for the B Method.
Pierre-Nicolas Tollitte
Extracting certified functional code from inductive specifications.
Mélanie Jacquel
Proof automation for the verification of Atelier B proof rules.
Jean-Frédéric Étienne
Certifying Airport Security Regulations using the Focal Environment.
Publications
Selected references
No publication matches this search.
Browse the complete PDF archive 30 documents
Talks & conferences
Sharing ideas
Invited talks, seminars and conference presentations, with slides from the former website.
Recent highlights
Proof Day · LIRMM Logic Group
Invited talk, Montpellier.
Science and Distrust
Panel discussion at MSH SUD, Montpellier.
World Logic Day
Talks in Montpellier.
EN Talks in English
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
ABZ'14 · Toulouse, France
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
GDR GPL · GT LTP · Bordeaux, France
Automated Deduction Modulo
PSATTT'13 · Invited talk · Palaiseau, France
Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover
Deducteam seminar · Paris, France
Assisting Users of Proof Assistants
HDR defence · Paris, France
Trusted Computer Mathematics within the Focalize Environment
MAP'10 · Logroño, Spain
A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations
UML&FM'08 · Kitakyushu-City, Japan
FR Talks in French
Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B
AFADL'14 · Paris, France
Benchmarks pour les projets de BWare
Réunion BWare · Paris, France
Animation de sémantiques formelles définies inductivement
Séminaire LIFL · Lille, France
Tableaux modulo théories en utilisant la superdéduction
Séminaire ICube · Strasbourg, France
Tableaux modulo théories en utilisant la superdéduction : une application à la vérification de règles de preuve B avec l'outil de démonstration automatique Zenon
Séminaire Loria · Nancy, France
Compilation de Focalize
Séminaire Deducteam · Paris, France
Séminaire ENSEEIHT
ENSEEIHT · Toulouse, France
Une introduction à l'environnement Focal
Journée Focal · Paris, France
Tutoriel Focal
JFLA'06 · Tutoriel invité · Pauillac, France
Teaching
From logic to safe software
University of Montpellier · Faculty of Science, with additional teaching at IMT Mines Alès.
Functional programming
OCaml · course created from scratch
First-order logic
Foundations and formal reasoning
Program verification
Programs and properties
Compilation
Including native MIPS code generation
Software security
Deductive methods and proof
Automated verification
Formal methods and tools
Academic service
Serving the community
Head of the PIPL team
LIRMM, Computer Science Department.
Head of the Computer Science Department
Faculty of Science, University of Montpellier.
Member of CNU Section 27
Qualifications, promotions, RIPEC and career reviews.
Head of the MaREL team
LIRMM, Computer Science Department.
Outreach, reviewing and committees
Hcéres evaluations, ANR reviews, PhD and habilitation committees, GJASE editorial board, GDR GPL thesis prize juries, and programme committees for AFADL, ASE, SETS, TABLEAUX, PxTP and other formal-methods events.
Beyond research
Mountains & expeditions
A personal archive of mountaineering, treks and expeditions.
For many years, mountaineering has been a great passion of mine. I am fortunate to live in France, at the heart of the European Alps and close to the Mont Blanc massif — a remarkable playground for alpinists.
My training was guided by Jean-Marie Ohl, a guide with the Association Internationale des Guides du Mont Blanc in Chamonix. My expedition experience was developed with Jean Annequin, a French mountain guide and expedition specialist.
Piton de la Fournaise
Réunion Island · 2,631 m
Mont Blanc
France · 4,807 m · Highest peak in the Alps
Kilimanjaro
Tanzania · 5,963 m · Highest peak in Africa
Ausangate
Peru · 6,384 m · Highest peak in the Cordillera Vilcanota
Aconcagua
Argentina · 6,962 m · Highest peak in the Americas
Teide
Tenerife · 3,718 m · Highest peak in Spain
Aragats
Armenia · 4,095 m · Highest peak in Armenia
La Soufrière
Guadeloupe · 1,467 m · Highest peak in Guadeloupe
Photo archive