Verifiable Properties of Database Transactions.

Michael Benedikt, Timothy Griffin, Leonid Libkin: Verifiable Properties of Database Transactions. PODS 1996: 117-127
  author    = {Michael Benedikt and
               Timothy Griffin and
               Leonid Libkin},
  title     = {Verifiable Properties of Database Transactions},
  booktitle = {Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium
               on Principles of Database Systems, June 3-5, 1996, Montreal,
  publisher = {ACM Press},
  year      = {1996},
  isbn      = {0-89791-781-2},
  pages     = {117-127},
  ee        = {, db/conf/pods/BenediktGL96.html},
  crossref  = {DBLP:conf/pods/96},
  bibsource = {DBLP,}


It is often necessary to ensure that database transactions preserve integrity constraints that specify valid database states. While it is possible to monitor for violations of constraints at run-time, rolling back transactions when violations are detected, it is preferable to verify correctness statically, before transactions are executed. This can be accomplished if we can verify transaction safety with respect to a set of constraints by means of calculating weakest preconditions. We study properties of weakest preconditions for a number of transaction and specification languages. We show that some simple transactions do not admit weakest preconditions over first-order logic. We also show that the class of transactions that admit weakest preconditions over first-order logic cannot be captured by any transaction language. We consider a strong local from of verifiability, and show that it is different from the general form. We define robustly verifiable transactions as those that can be statically analyzed regardless of extensions to the signature of the specification language, and we show that the class of robustly verifiable transactions over first order logic is exactly the class of transactions that admit the local form of verifiability. We discuss the implications of these results for the design of verifiable transaction languages.

Copyright © 1996 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

Load The ACM SIGMOD Anthology, CDROM Edition, Volume 1-3, PODS '82-'98. and ... Load The ACM SIGMOD Anthology, Silver Edition, DVD 1, Proceedings. and ... BibTeX

Printed Edition

Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 3-5, 1996, Montreal, Canada. ACM Press 1996, ISBN 0-89791-781-2
Contents BibTeX

Online Edition: ACM Digital Library

[Index Terms]
[Full Text in PDF Format, 1048 KB]


Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley 1995, ISBN 0-201-53771-0
Contents BibTeX
Serge Abiteboul, Victor Vianu: Transactions and Integrity Constraints. PODS 1985: 193-204 BibTeX
Serge Abiteboul, Victor Vianu: Procedural Languages for Database Queries and Updates. J. Comput. Syst. Sci. 41(2): 181-229(1990) BibTeX
Serge Abiteboul, Victor Vianu: Datalog Extensions for Database Queries and Updates. J. Comput. Syst. Sci. 43(1): 62-124(1991) BibTeX
Ralph-Johan Back: Proving Total Correctness of Nondeterministic Programs in Infinitary Logic. Acta Inf. 15: 233-249(1981) BibTeX
Michael Benedikt, Guozhu Dong, Leonid Libkin, Limsoon Wong: Relational Expressive Power of Constraint Query Languages. PODS 1996: 5-16 BibTeX
Rudolf Berghammer, Birgit Elbl, Ulf R. Schmerl: Formalizing Dijkstra's Predicate Transformer wp in Weak Second-Order Logic. Theor. Comput. Sci. 146(1&2): 185-197(1995) BibTeX
Val Tannen, Ramesh Subrahmanyam: Logical and Computational Aspects of Programming with Sets/Bags/Lists. ICALP 1991: 60-75 BibTeX
Edsger W. Dijkstra: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8): 453-457(1975) BibTeX
Edsger W. Dijkstra: A Discipline of Programming. Prentice-Hall 1976
Ronald Fagin: Finite-Model Theory - A Personal Perspective. Theor. Comput. Sci. 116(1&2): 3-31(1993) BibTeX
Ronald Fagin, Larry J. Stockmeyer, Moshe Y. Vardi: On Monadic NP vs. Monadic co-NP. Inf. Comput. 120(1): 78-92(1995) BibTeX
Arding Hsu, Tomasz Imielinski: Integrity Checking for Multiple Updates. SIGMOD Conference 1985: 152-168 BibTeX
Neil Immerman: Languages that Capture Complexity Classes. SIAM J. Comput. 16(4): 760-778(1987) BibTeX
Neil Immerman, Sushant Patnaik, David W. Stemple: The Expressiveness of a Family of Finite Set Languages. PODS 1991: 37-52 BibTeX
Dino Karabeg, Victor Vianu: Simplification Rules and Complete Axiomatization for Relational Update Transactions. ACM Trans. Database Syst. 16(3): 439-475(1991) BibTeX
Leonid Libkin, Limsoon Wong: New Techniques for Studying Set Languages, Bag Languages and Aggregate Functions. PODS 1994: 155-166 BibTeX
Leonid Libkin, Limsoon Wong: Some Properties of Query Languages for Bags. DBPL 1993: 97-114 BibTeX
William McCune, Lawrence J. Henschen: Maintaining state constraints in relational databases: a proof theoretic basis. J. ACM 36(1): 46-68(1989) BibTeX
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
Xiaolei Qian: An Effective Method for Integrity Constraint Simplification. ICDE 1988: 338-345 BibTeX
Xiaolei Qian: An Axiom System for Database Transactions. Inf. Process. Lett. 36(4): 183-189(1990) BibTeX
Xiaolei Qian: The Expressive Power of the Bounded-Iteration Construct. Acta Inf. 28(7): 631-656(1991) BibTeX
Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989) BibTeX
David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386 BibTeX

Referenced by

  1. Timothy Griffin, Richard Hull: A Framework for Implementing Hypothetical Queries. SIGMOD Conference 1997: 231-242
  2. Michael Benedikt, H. Jerome Keisler: Expressive Power of Unary Counters. ICDT 1997: 291-305
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:34:15 2009