DAHU: Verification and Databases

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.

Members

Permanent Members

Serge Abiteboul
Senior researcher, INRIA Saclay-Île de France
Florent Jacquemard
Researcher, INRIA
Cristina Sirangelo
Assistant professor, ENS Cachan
Stéphane Demri
Senior researcher, CNRS
Luc Segoufin
Senior researcher, INRIA
 

Associated and Temporary Members

Yannis Katsis
Researcher, INRIA Saclay-Île de France
 

Ph.D. Students

Pierre Bourhis
PhD student
Alban Galland
PhD student, INRIA
Thomas Place
PhD student, ENS Cachan
Diego Figueira
PhD student, INRIA
Wojciech Kazana
PhD student, INRIA
Camille Vacher
PhD student, France Telecom & ENS Cachan

More

Dahu participates in the EU FP7 project FOX: FOX.
Dahu also participates in the ERC advance grant Webdam: Webdam.

Dahu participates in the French ANR grant ENUM and the French ANR grant Averiss.

About LSV

About Dahu

Logo DAHU

A joint team with

Logo INRIA Saclay

Recent Publications

All the Dahu publications

D. Figueira, P. Hofman and S. LasotaRelating timed and register automataIn EXPRESS'10.  2010. To appear. PDF | BibTeX )
S. DemriOn Selective Unboundedness of VASSIn INFINITY'10, Electronic Proceedings in Theoretical Computer Science.  2010. To appear. PDF | BibTeX )
D. Figueira, S. Figueira, S. Schmitz and Ph. SchnoebelenAckermann and Primitive-Recursive Bounds with Dickson's Lemma.  Research Report cs.LO/1007.2989, Computing Research Repository,  2010. Web page | PDF | BibTeX )
G. Fontaine and Th. PlaceClasses of trees definable in the μ-calculusIn MFCS'10, LNCS 6281, pages 381-392. Springer,  2010. BibTeX )
N. Schweikart and L. SegoufinAddition-invariant FO and regularityIn LICS'10. IEEE Computer Society Press,  2010. To appear. PDF | BibTeX )

All the Dahu publications