ACM SIGMOD Anthology TODS dblp.uni-trier.de

Automatic Verification of Database Transaction Safety.

Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989)
@article{DBLP:journals/tods/SheardS89,
  author    = {Tim Sheard and
               David W. Stemple},
  title     = {Automatic Verification of Database Transaction Safety},
  journal   = {ACM Trans. Database Syst.},
  volume    = {14},
  number    = {3},
  year      = {1989},
  pages     = {322-368},
  ee        = {http://doi.acm.org/10.1145/68012.68014, db/journals/tods/SheardS89.html},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX

Abstract

Maintaining the integrity of databases is one of the promises of database management systems. This includes assuring that integrity constraints are invariants of database transactions. This is very difficult to accomplish efficiently in the presence of complex constraints and large amounts of data. One way to minimize the amount of processing required to maintain database integrity over transaction processing is to prove at compile-time that transactions cannot, if run atomically, disobey integrity constraints. We report on a system that performs such verification for a robust set of constraint and transaction classes. The system accepts database schemas written in a more or less traditional style and accepts programs in a high-level programming language.

Copyright © 1989 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.

Joint ACM SIGMOD / IEEE Computer Society Anthology

CDROM Version: Load the CDROM "Volume 3 Issue 1, TODS 1976-1990" and ... DVD Version: Load ACM SIGMOD Anthology DVD 2" and ... BibTeX

References

[1]
Philip A. Bernstein, Barbara T. Blaustein: Fast Methods for Testing Quantified Relational Calculus Assertions. SIGMOD Conference 1982: 39-50 BibTeX
[2]
...
[3]
Marco A. Casanova, Philip A. Bernstein: The Logic of a Relational Data Manipulation Language. POPL 1979: 101-109 BibTeX
[4]
Marco A. Casanova, Philip A. Bernstein: A Formal System for Reasoning about Programs Accessing a Relational Database. ACM Trans. Program. Lang. Syst. 2(3): 386-414(1980) BibTeX
[5]
Richard A. DeMillo, Richard J. Lipton, Alan J. Perlis: Social Processes and Proofs of Theorems and Programs. Commun. ACM 22(5): 271-280(1979) BibTeX
[6]
Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX
[7]
John V. Guttag: Notes on Type Abstraction (Version 2). IEEE Trans. Software Eng. 6(1): 13-23(1980) BibTeX
[8]
Lawrence J. Henschen, William McCune, Shamim A. Naqvi: Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory 1982: 145-169 BibTeX
[9]
C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) BibTeX
[10]
...
[11]
Arding Hsu, Tomasz Imielinski: Integrity Checking for Multiple Updates. SIGMOD Conference 1985: 152-168 BibTeX
[12]
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
[13]
Derek C. Oppen: Reasoning about Recursively Defined Data Structures. POPL 1978: 151-157 BibTeX
[14]
N. C. K. Phillips: Safe Data Type Specifications. IEEE Trans. Software Eng. 10(3): 285-290(1984) BibTeX
[15]
Tim Sheard, David W. Stemple: Coping with Complexity in Automated Reasoning about Database Systems. VLDB 1985: 426-435 BibTeX
[16]
...
[17]
David W. Stemple, Tim Sheard: Specification and Verification of Abstract Database Types. PODS 1984: 248-257 BibTeX
[18]
David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386 BibTeX
[19]
...
[20]
David W. Stemple, Tim Sheard, Ralph E. Bunker: Abstract Data Types in Databases: Specification, Manipulation and Access. ICDE 1986: 590-597 BibTeX
[21]
...

Referenced by

  1. Suad Alagic: A Family of the ODMG Object Models. ADBIS 1999: 14-30
  2. Véronique Benzaken, Xavier Schaefer: Static Management of Integrity in Object-Oriented Databases: Design and Implementation. EDBT 1998: 311-325
  3. David Spelt, Herman Balsters: Automatic Verification of Transactions on an Object-Oriented Database. DBPL 1997: 396-412
  4. Michael Benedikt, Timothy Griffin, Leonid Libkin: Verifiable Properties of Database Transactions. PODS 1996: 117-127
  5. Dimitris Plexousakis, John Mylopoulos: Accomodating Integrity Constraints During Database Design. EDBT 1996: 497-513
  6. Véronique Benzaken, Anne Doucet: Thémis: A Database Programming Language Handling Integrity Constraints. VLDB J. 4(3): 493-517(1995)
  7. Malcolm P. Atkinson, Ronald Morrison: Orthogonally Persistent Object Systems. VLDB J. 4(3): 319-401(1995)
  8. Stefano Ceri, Piero Fraternali, Stefano Paraboschi, Letizia Tanca: Automatic Generation of Production Rules for Integrity Maintenance. ACM Trans. Database Syst. 19(3): 367-422(1994)
  9. Subhasish Mazumdar, David W. Stemple: Helping the Database Designer Maintain Inegrity Constraints. IEEE Data Eng. Bull. 17(2): 28-32(1994)
  10. Paul W. P. J. Grefen, Rolf A. de By, Peter M. G. Apers: Integrity Control in Advanced Database Systems. IEEE Data Eng. Bull. 17(2): 9-13(1994)
  11. Val Tannen: Tutorial: Languages for Collection Types. PODS 1994: 150-154
  12. Alexandre V. Zamulin: From a Database Programming Language to a Database Specification Language (Invited Paper). ADBIS 1994: 122-131
  13. Xiaolei Qian: The Deductive Synthesis of Database Transactions. ACM Trans. Database Syst. 18(4): 626-677(1993)
  14. Véronique Benzaken, Anne Doucet: Thémis: a database programming language with integrity constraints. DBPL 1993: 243-262
  15. Subhasish Mazumdar: Optimizing Distributed Integrity Constraints. DASFAA 1993: 327-334
  16. H. V. Jagadish, Xiaolei Qian: Integrity Maintenance in Object-Oriented Databases. VLDB 1992: 469-480
  17. Neil Immerman, Sushant Patnaik, David W. Stemple: The Expressiveness of a Family of Finite Set Languages. PODS 1991: 37-52
  18. Leonidas Fegaras, David W. Stemple: Using Type Transformation in Database Implementation. DBPL 1991: 337-353
  19. Xiaolei Qian: Synthesizing Database Transactions. VLDB 1990: 552-565
  20. Manfred A. Jeusfeld, Michael Mertikas, Ingrid Wetzel, Matthias Jarke, Joachim W. Schmidt: Database Application Development as an Object Modeling Activity. VLDB 1990: 442-454
  21. David W. Stemple, Leonidas Fegaras, Tim Sheard, Adolfo Socorro: Exceeding the Limits of Polymorphism in Database Programming Languages. EDBT 1990: 269-285
  22. Leonidas Fegaras, Tim Sheard, David W. Stemple: The ADABTPL Type System. DBPL 1989: 207-218
  23. Xiaolei Qian, Richard J. Waldinger: A Transaction Logic for Database Specification. SIGMOD Conference 1988: 243-250
  24. Subhasish Mazumdar, David W. Stemple, Tim Sheard: Resolving the Tension between Integrity and Security Using a Theorem Prover. SIGMOD Conference 1988: 233-242
  25. David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386
  26. W. Bruce Croft, David W. Stemple: Supporting Offics Document Architectures with Constrained Types. SIGMOD Conference 1987: 504-509
  27. David W. Stemple, Tim Sheard: Construction and Calculus of Types for Database Systems. DBPL 1987: 3-22
BibTeX
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
TODS, ACM SIGMOD Anthology: Copyright © by ACM (info@acm.org), Corrections: anthology@acm.org
DBLP: Copyright © by Michael Ley (ley@uni-trier.de), last change: Tue Jun 24 18:39:06 2008