Campus Event Calendar
Event Entry
What and Who
Databases Meet Verification: What do we have in common, and how can we help each other?
Prof Dr Leonid Libkin
School of Informatics, Uni Edinburgh
Distinguished Speaker Series Max
Planck Institute for Informatics and Cluster of Excellence Multimodal Computing and Interaction
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 17 June 2008
13:00
45 Minutes
E1 4
024
Saarbrücken
Abstract
The main computational tasks in the fields of databases and verification
can be summarized as evaluation of logical formulae on finite (or
sometimes infinite but finitely presented) structures. And yet the
differences in logics and types of structures have kept these fields
further apart than they should be. This is changing now, partly due to
more flexible data formats, such as XML, taking the central role in
database research. Navigation over XML documents closely resembles
temporal properties used in software verification, which bridges the gap
between tools and techniques used in the two fields.
In this talk, I explain how (and why) the fields of databases and
verification developed largely independent of each other, and give
examples of data processing problems where model-checking techniques
could be used. I then concentrate on an example of the converse: we look
at nested words, which serve as a nice abstraction for reasoning about
programs with recursive procedure calls. I show how results on the XML
navigation language XPath can be applied in this context to get
expressively complete logics for nested words with good model-checking
properties.
can be summarized as evaluation of logical formulae on finite (or
sometimes infinite but finitely presented) structures. And yet the
differences in logics and types of structures have kept these fields
further apart than they should be. This is changing now, partly due to
more flexible data formats, such as XML, taking the central role in
database research. Navigation over XML documents closely resembles
temporal properties used in software verification, which bridges the gap
between tools and techniques used in the two fields.
In this talk, I explain how (and why) the fields of databases and
verification developed largely independent of each other, and give
examples of data processing problems where model-checking techniques
could be used. I then concentrate on an example of the converse: we look
at nested words, which serve as a nice abstraction for reasoning about
programs with recursive procedure calls. I show how results on the XML
navigation language XPath can be applied in this context to get
expressively complete logics for nested words with good model-checking
properties.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 06/16/2008 10:40
Roxane Wetzel, 06/04/2008 12:07
Roxane Wetzel, 05/30/2008 13:32
Roxane Wetzel, 05/30/2008 13:04 -- Created document.
Roxane Wetzel, 06/04/2008 12:07
Roxane Wetzel, 05/30/2008 13:32
Roxane Wetzel, 05/30/2008 13:04 -- Created document.