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, INRIA
Alban Galland
PhD student, INRIA
Thomas Place
PhD student, ENS Cachan
Diego Figueira
PhD student, INRIA
Wojciech Kazana
PhD student, INRIA
 

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

S. Demri and D. LugiezComplexity of Modal Logics with Presburger ConstraintsJournal of Applied Logic, 2010. To appear. PDF | BibTeX )
L. Libkin and C. SirangeloReasoning about XML with temporal logics and automataJournal of Applied Logic 8(2), pages 210-232,  2010. PDF | BibTeX )
S. Demri, R. Lazic and A. SangnierModel checking memoryful linear-time logics over one-counter automataTheoretical Computer Science, 2010. To appear. PDF | BibTeX )
B. ten Cate and L. SegoufinTransitive Closure Logic, Nested Tree Walking Automata, and XPathJournal of the ACM, 2010. To appear. PDF | BibTeX )
M. Bojanczyk, A. Muscholl, Th. Schwentick and L. SegoufinTwo-variable logic on data trees and applications to XML reasoningJournal of the ACM 56(3),  2009. PDF | BibTeX )

All the Dahu publications