Personal tools
You are here: Home Events LFCS seminar: Stefania Dumbrava: Certifying deductive database engines with Coq/SSReflect

LFCS seminar: Stefania Dumbrava: Certifying deductive database engines with Coq/SSReflect

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Nov 14, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal

Deductive databases extend relational ones with inference and with the ability to seamlessly handle more complex (recursive) queries. Their underlying language, Datalog, is purely declarative and captures the function-free fragment of Horn predicate logic. Traditionally seen as a toy-language for theoreticians, Datalog has recently regained popularity, due to the emergence of new application domains and successful commercial implementations. With increasingly complex systems and applications being built on top of Datalog engines, ensuring their safe and reliable functioning has become crucial.

These strong guarantees can be obtained using formal methods and tools. In particular, we envisage a methodology aimed at certifying realistic deductive database engines by refinement, using the Coq/SSReflect proof assistant. This would encompass: (1) a high-level formalization suitable for proof-development and, thus, employing more inefficient algorithms, (2) a mechanization of real-world implementations, and (3) (refinement) proofs of their extensional equivalence.

In this talk, we will focus on the first, necessary, step in this direction. As such, we will detail the proof-engineering efforts involved in certifying a standard Datalog engine and its extension with stratified negation. The developed library contains a formalization of their model theoretic and fixpoint semantics - implemented through bottom-up and, respectively, through stratified evaluation procedures - as well as the corresponding soundness and termination, completeness and model minimality proofs. We expand on the material published at ITP 2017 and in my PhD thesis.


Document Actions