Verifiable Properties of Database Transactions

Summary: Proves some transactions lack first-order weakest preconditions (WPs) and that the class of WP-admitting transactions cannot be captured by any transaction language. Introduces local vs. robust verifiability and shows robust FO verifiability exactly equals the local form, with implications for verifiable transaction-language design. (summarized by gpt-5-mini on Feb 09 2026)

Paper ID: h56d8114dde51e714
Venue: PODS
Year: 1996
Pagerank: 6.0703115e-05
Overall Rank: 5,602 | 62.34%
DOI: 10.1145/237661.237692

Incoming Non-self Citations Over Time

Authors

1. Michael Benedikt (AT&T)
2. Timothy Griffin (AT&T)
3. Leonid Libkin (AT&T)

BibTeX Citation

@inproceedings{benedikt_pods96,
        address = {New York, NY, USA},
        series = {{PODS} '96},
        title = {{Verifiable Properties of Database Transactions}},
        url = {https://dl.acm.org/doi/10.1145/237661.237692},
        doi = {10.1145/237661.237692},
        booktitle = {Proceedings of the {ACM} {SIGMOD} Symposium on {Principles} of {Database} {Systems}},
        publisher = {Association for Computing Machinery},
        author = {Benedikt, Michael and Griffin, Timothy and Libkin, Leonid},
        year = {1996}
}

Incoming Citations (Sorted by Pagerank)

Showing 3 of 3 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank
1,136	BlockchainDB - A Shared Database on Blockchains	2019	VLDB	0.00011875973
2,711	Foundations of Data-Aware Process Analysis: A Database Theory Perspective	2013	PODS	8.1038896e-05
3,048	A Framework for Implementing Hypothetical Queries	1997	SIGMOD	7.7095211e-05

Outgoing Citations (Sorted by Pagerank)

Showing 5 of 5 cited papers.

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

Rank	Cited Paper	Year	Venue	Pagerank
1,919	The Expressiveness of a Family of Finite Set Languages	1991	PODS	9.3781849e-05
1,950	Relational Expressive Power of Constraint Query Languages	1996	PODS	9.3195393e-05
5,042	On the Modes and Meaning of Feedback to Transaction Designers	1987	SIGMOD	6.3002599e-05
5,082	Transactions And Integrity Constraints	1985	PODS	6.2847136e-05
8,005	New Techniques for Studying Set Languages, Bag Languages and Aggregate Functions	1994	PODS	5.4085878e-05

Semantically Similar Papers

#	Overall Rank	Paper	Year	Venue
1	1,767	A Transaction Language Complete for Database Update and Specification	1987	PODS
2	8,674	Checking Consistency of Database Constraints: a Logical Basis	1986	VLDB
3	10,137	Deciding Robustness for Lower SQL Isolation Levels	2020	PODS
4	9,270	On Correctness of Non-serializable Executions	1993	PODS
5	11,835	Robustness Against Read Committed: A Free Transactional Lunch	2022	PODS
6	5,042	On the Modes and Meaning of Feedback to Transaction Designers	1987	SIGMOD
7	11,044	Fast Verification of Strong Database Isolation	2026	VLDB
8	13,522	Specification and Verification of Abstract Database Types	1984	PODS
9	5,082	Transactions And Integrity Constraints	1985	PODS
10	7,595	A Transaction Logic for Database Specification	1988	SIGMOD