A Coq formalization of data provenance

Benzaken, Véronique ; Cohen-Boulakia, Sarah ; et al.

In: Certified Programs and Proofs ; https://hal.science/hal-03380459 ; Certified Programs and Proofs, ACM, Jan 2021, Virtual Event, Denmark. ⟨10.1145/3437992.3439920⟩ ; https://dl.acm.org/doi/proceedings/10.1145/3437992, 2021

Online Konferenz

Wie komme ich dran?

Zugriff:

Volltext

International audience ; In multiple domains, large amounts of data are daily generated and combined to be analyzed. The interpretation of these analyses requires to track back the provenance of combined data with respect to initial, raw data. The correctness of the provenance is crucial in many critical domains, such as medicine to prescribe treatments. In this article, we propose the first provenance-aware extended relational algebra formalized in a proof assistant (Coq), for a non trivial subset of database queries: queries containing aggregates, null values, and correlated sub-queries. The formalization is validated by an adequacy proof with respect to standard evaluation of queries. This development is a first step towards a posteriori certification of provenance for data manipulation, with strong guaranties.

Titel:	A Coq formalization of data provenance
Autor/in / Beteiligte Person:	Benzaken, Véronique ; Cohen-Boulakia, Sarah ; Contejean, Évelyne ; Keller, Chantal ; Zucchini, Rébecca ; Paris-Saclay, Université ; Centre National de la Recherche Scientifique (CNRS) ; Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; École normale supérieure - Cachan (ENS Cachan) ; ACM ; Cătălin Hriţcu and Andrei Popescu ; ANR-15-CE39-0009,DataCert,Spécification intensive en Coq d'intégration de données orientée sécurité(2015)
Link:	https://hal.science/hal-03380459 https://hal.science/hal-03380459/document Volltext https://doi.org/10.1145/3437992.3439920 https://doi.org/10.1145/3437992
Zeitschrift:	Certified Programs and Proofs ; https://hal.science/hal-03380459 ; Certified Programs and Proofs, ACM, Jan 2021, Virtual Event, Denmark. ⟨10.1145/3437992.3439920⟩ ; https://dl.acm.org/doi/proceedings/10.1145/3437992, 2021
Veröffentlichung:	HAL CCSD ; ACM, 2021
Medientyp:	Konferenz
DOI:	10.1145/3437992.3439920
Schlagwort:	Virtual Event Denmark CCS Concepts: • Software and its engineering → Formal software verification Correctness Software verification • Theory of computation → Logic and verification Type theory Program verification Program semantics Data provenance extended relational algebra Coq [INFO]Computer Science [cs] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Subject Geographic: Virtual Event Denmark
Sonstiges:	Nachgewiesen in: BASE Sprachen: English Document Type: conference object Language: English Relation: hal-03380459; https://hal.science/hal-03380459; https://hal.science/hal-03380459/document; https://hal.science/hal-03380459/file/cpp21.pdf Rights: info:eu-repo/semantics/OpenAccess

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.