DAHU: Databases and Verification

The need to access and exchange data on the Web has led to database management systems (DBMS) that are increasingly distributed and autonomous. Data extraction and querying on the Web is harder than in classical DBMS, because such data is heterogeneous, redundant, inconsistent and subject to frequent modifications. DBMS thus need to be able to detect errors, to analyze them and to correct them. Moreover, increasingly complex Web applications and services rely on DBMS, and their reliability is crucial. This creates a need for tools for specifying DBMS in a high-level manner that is easier to understand, while also facilitating verification of critical properties.

The study of such specification and verification techniques is the main goal of Dahu.


Permanent Members

Serge Abiteboul
Senior researcher, INRIA Saclay-Île de France
Sylvain Schmitz
Assistant professor, ENS Cachan
Luc Segoufin
Senior researcher, INRIA Saclay-Île de France

Associated and Temporary Members

Karima Rafes
PhD student, BorderCloud
Victor Vianu
Researcher, chaire INRIA (professor, UC San Diego)
Alexandre Vigny
PhD student (joint with Paris 7)

Ph.D. Students

Nathan Grosshans
PhD student, Digiteo (joint with U. Montreal, Canada)
David Montoya
PhD student, INRIA & Cofely INEO
Anthony Lick
PhD student, ANR Prodaq
Su Yang
PhD student


About LSV

About Dahu

A joint team with

Logo INRIA Saclay

Recent Publications

All the Dahu publications

T. Place and L. SegoufinDecidable Characterization of FO2(<, +1) and locality of DA.  Research Report abs/1606.03217, Computing Research Repository, June 2016. 8 pages. PDF | BibTeX )
F. Jacquemard, L. Segoufin and J. DiminoFO2(<, +1, extasciitilde) on data trees, data tree automata and branching vector addition systemsLogical Methods in Computer Science 12(2), 2016. Web page | PDF | BibTeX )
J. Goubault-Larrecq and S. SchmitzDeciding Piecewise Testable Separability for Regular Tree LanguagesIn ICALP'16, Leibniz International Proceedings in Informatics 55, pages 97:1-97:15. Leibniz-Zentrum für Informatik, July 2016. Web page | BibTeX )
R. Lazić and S. SchmitzThe Complexity of Coverability in ν-Petri NetsIn LICS'16. ACM Press, July 2016. To appear. Web page | BibTeX )
Th. Place and L. SegoufinDeciding definability in FO2(<h,<v) on treesLogical Methods in Computer Science 11(3:5), September 2015. PDF | BibTeX )

All the Dahu publications