by Leonid Libkin
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 (the second part of the talk is based on a joint paper with Alur, Arenas, Barcelo, Etessami, and Immerman from LICS 2007).