Personal tools
You are here: Home Graduate Study Databases and Verification

Databases and Verification

The basic settings of the fields of database querying and verification/model-checking are very similar: in both cases one evaluates a logical formula on a finite structure (a query on a relational database, or a temporal formula on a Kripke structure). Both fields have invested heavily in developing logical formalisms and efficient algorithms for query evaluation and model checking, but despite this, there are very few direct connections between them (for example, we now know how temporal logics and navigation in XML documents are related). There are many more potential connections that have not received the attention they deserve: e.g., between streaming XML and verification of pushdown specifications or between database querying and verifying data-driven web services. One of my goals is to study these connections, with the ultimate goal of bringing the fields closer together. I am interested in students with good theoretical background (logic, automata, algorithms); knowledge of databases and verification is obviously a plus.


Prospective Supervisors

Leonid Libkin

Document Actions