Specification and Verification of Abstract Database Types

Summary: Models a DB (schema, constraints, transactions, queries) as an ADT whose values are legal database states and defines transaction safety as closure on that state set. Provides a designer-friendly spec and adapts Boyer–Moore proving by encoding transactions as recursive-list functions for mechanical safety proofs. (summarized by gpt-5-mini on Feb 09 2026)

Paper ID: 704
Venue: PODS
Year: 1984
Pagerank: 5.093636e-05
Overall Rank: 13,232 | 9.22%
DOI: 10.1145/588011.588047

Incoming Non-self Citations Over Time

No non-self incoming citations found for this paper in this database.

Authors

1. David Stemple (University of Massachusetts Amherst)
2. Tim Sheard (University of Massachusetts Amherst)

BibTeX Citation

@inproceedings{stemple_pods84,
        address = {New York, NY, USA},
        series = {{PODS} '84},
        title = {{Specification and Verification of Abstract Database Types}},
        url = {https://dl.acm.org/doi/10.1145/588011.588047},
        doi = {10.1145/588011.588047},
        booktitle = {Proceedings of the {ACM} {SIGMOD} Symposium on {Principles} of {Database} {Systems}},
        publisher = {Association for Computing Machinery},
        author = {Stemple, David and Sheard, Tim},
        year = {1984}
}

Incoming Citations (Sorted by Pagerank)

Showing 2 of 2 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank
4,923	On the Modes and Meaning of Feedback to Transaction Designers	1987	SIGMOD	6.4441344e-05
13,226	Coping with Complexity in Automated Reasoning about Database Systems	1985	VLDB	5.093636e-05

Outgoing Citations (Sorted by Pagerank)

Showing 3 of 3 cited papers.

Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.

Rank	Cited Paper	Year	Venue	Pagerank
247	Some High-level Language Constructs for Data of Type Relation	1977	SIGMOD	0.00023302214
541	Efficient Monitoring of Database Assertions	1978	SIGMOD	0.00016860824
1,624	Fast Methods For Testing Quantified Relational Calculus Assertions	1982	SIGMOD	0.00010194403

Semantically Similar Papers

#	Overall Rank	Paper	Year	Venue
1	13,073	Combining Theory and Practice in Integrity Control: A Declarative Approach to the Specification of a Transaction Modification Subsystem	1993	VLDB
2	4,923	On the Modes and Meaning of Feedback to Transaction Designers	1987	SIGMOD
3	5,081	A Temporal Framework for Database Specification and Verification	1984	VLDB
4	6,196	On Verification Of Database Temporal Constraints	1985	SIGMOD
5	14,419	Synthesizing Database Transactions	1990	VLDB
6	4,962	Transactions And Integrity Constraints	1985	PODS
7	5,475	Verifiable Properties of Database Transactions	1996	PODS
8	8,564	Resolving the Tension between Integrity and Security Using a Theorem Prover	1988	SIGMOD
9	7,452	A Transaction Logic for Database Specification	1988	SIGMOD
10	13,226	Coping with Complexity in Automated Reasoning about Database Systems	1985	VLDB