up: Publications

Reasoning Formally about Database Queries and Updates

Jon Haël Brenas, Rachid Echahed, Martin Strecker


This paper explores formal verification in the area of database technology, in particular how to reason about queries and updates in a database system. The formalism is sufficiently general to be applicable to relational and graph databases. We first define a domain-specific language consisting of nested query and update primitives, and give its operational semantics. Queries are in full first-order logic. The problem we try to solve is whether a database satisfying a given pre-condition will satisfy a given post-condition after execution of a given sequence of queries and updates. We propose a weakest-precondition calculus and prove its correctness. We finally examine a restriction of our framework that produces formulas in the guarded fragment of predicate logic and thus leads to a decidable proof problem.
 Online Copy

BibTeX Entry

  author =    {Jon Haël Brenas and Rachid Echahed and Martin Strecker},
  title =     {Reasoning Formally about Database Queries and Updates},
  booktitle = {FM'2019},
  year =      2019,
  editor =    {Maurice ter Beek and Annabelle McIver and José Oliveira},
  series =    {LNCS},
  publisher = {Springer},
  url       = {http://martin-strecker.org/Publications/fm2019.html},
  note =      {to appear}

Last modified: Mon Aug 12 17:51:53 CEST 2019