Certified Graph View Maintenance with Regular Datalog
In: ISSN: 1471-0684, 2018
Online
academicJournal
Zugriff:
International audience ; We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD)-a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism , we test an OCaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines.
Titel: |
Certified Graph View Maintenance with Regular Datalog
|
---|---|
Autor/in / Beteiligte Person: | Bonifati, Angela ; Dumbrava, Stefania ; Gallego Arias, Emilio Jesús ; Base de Données (BD) ; Laboratoire d'InfoRmatique en Image et Systèmes d'information (LIRIS) ; Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL) ; Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Institut National des Sciences Appliquées de Lyon (INSA Lyon) ; Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL) ; Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS) ; Mines Paris - PSL (École nationale supérieure des mines de Paris) ; Université Paris Sciences et Lettres (PSL) ; Centre de Recherche en Informatique (CRI) ; Université Paris Sciences et Lettres (PSL)-Université Paris Sciences et Lettres (PSL) ; ANR-11-IDEX-0007,Avenir L.S.E.,PROJET AVENIR LYON SAINT-ETIENNE(2011) |
Link: | |
Zeitschrift: | ISSN: 1471-0684, 2018 |
Veröffentlichung: | HAL CCSD ; Cambridge University Press (CUP), 2018 |
Medientyp: | academicJournal |
DOI: | 10.1017/S1471068418000224 |
Schlagwort: |
|
Sonstiges: |
|