This page contains
Current data management applications and systems involve increasingly massive data volumes. Surprisingly, while the amount of data stored and managed by data engines has drastically increased, little attention has been devoted to ensure that those are reliable. Obtaining strong guarantees requires the use of formal methods and mature tools. A very promising approach consists in using proof assistants such as Coq [1,2]. Our purpose is to prove that existing systems conform to their specifications and to verify that programs that make intensive use of database queries and transactions are correct. This internship leads to a PhD if the candidate demonstrates the expected skills.
Concurency control is one of cornerstone of database systems as it is at the heart of transaction processing management. Many different concurency models and protocols have been proposed over the last decades. None of them have been formally specified nor been proven correct. Building on the work in  and based on the specification given in , the candidate will formalize in Coq different concurrency models (semantics and properties) and verify the corresponding algorithms and/protocols.