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: hba5b299a19fdb3e5
Venue: PODS
Year: 1984
Pagerank: 4.9793485e-05
Overall Rank: 13,522 | 9.09%
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
5,042	On the Modes and Meaning of Feedback to Transaction Designers	1987	SIGMOD	6.3002599e-05
13,516	Coping with Complexity in Automated Reasoning about Database Systems	1985	VLDB	4.9793485e-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
263	Some High-level Language Constructs for Data of Type Relation	1977	SIGMOD	0.00022811354
554	Efficient Monitoring of Database Assertions	1978	SIGMOD	0.00016521437
1,656	Fast Methods For Testing Quantified Relational Calculus Assertions	1982	SIGMOD	9.9690086e-05

Semantically Similar Papers

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