Room 206 (2nd floor, badged access)
23 November 2021 - 14h00
Design, Development and certification in Coq/MathComp of Datalog optimizations for network verification (Phd Defense)
by PIERRE-LEO BEGAY from Orange Labs & Verimag
Abstract: We introduce a static analysis and two program transformations for Datalog to circumvent performance issues that arise with the implementation of primitive predicates, notably in the framework of a large scale telecommunication application. This analysis and the rewritings are certified using DatalogCert, an existing Coq/MathComp formalization of Datalog. To this effect, we introduce a new trace semantics for Datalog with a verified mechanization. This work can be seen as both a first step and proof of concept for the creation of a full-blown library of verified Datalog optimizations using DatalogCert, towards the development of a realistic environment for certified data-centric applications.
