VerIso: Verifiable Isolation Guarantees for Database Transactions
Summary: VerIso—an Isabelle/HOL framework—provides the first mechanized, mathematically rigorous toolchain to model transactions and verify isolation guarantees over all system behaviors. Applied to S2PL it proves strict serializability and uncovers new counterexamples showing TAPIR violates claimed strict serializability and even atomic visibility. (summarized by gpt-5-mini on Feb 09 2026)
Incoming Non-self Citations Over Time
No non-self incoming citations found for this paper in this database.
Authors
- 1. Shabnam Ghasemirad (ETH Zurich)
- 2. Si Liu (ETH Zurich)
- 3. Christoph Sprenger (ETH Zurich)
- 4. Luca Multazzu (ETH Zurich)
- 5. David Basin (ETH Zurich)
BibTeX Citation
@article{ghasemirad_vldb25,
title = {{VerIso: Verifiable Isolation Guarantees for Database Transactions}},
author = {Ghasemirad, Shabnam and Liu, Si and Sprenger, Christoph and Multazzu, Luca and Basin, David},
journal = {PVLDB},
series = {{VLDB} '25},
volume = {18},
number = {5},
pages = {1362--1375},
doi = {10.14778/3718057.3718065},
url = {https://doi.org/10.14778/3718057.3718065},
year = {2025}
}Incoming Citations (Sorted by Pagerank)
Showing 2 of 2 citing papers.
| Rank | Citing Paper | Year | Venue | Pagerank |
|---|---|---|---|---|
| 10,331 | Testing Graph Databases with Synthesized Queries | 2026 | SIGMOD | 5.093636e-05 |
| 10,597 | Fast Verification of Strong Database Isolation | 2026 | VLDB | 5.093636e-05 |
Previous
Page 1 / 1
Next
Outgoing Citations (Sorted by Pagerank)
Showing 9 of 9 cited papers.
Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.
| Rank | Cited Paper | Year | Venue | Pagerank |
|---|---|---|---|---|
| 19 | A Critique of ANSI SQL Isolation Levels | 1995 | SIGMOD | 0.00058720861 |
| 1,080 | Elle: Inferring Isolation Anomalies from Experimental Observations | 2021 | VLDB | 0.00012257972 |
| 1,961 | Scalable Atomic Visibility with RAMP Transactions | 2014 | SIGMOD | 9.4000927e-05 |
| 4,274 | Causal Consistency and Latency Optimality: Friend or Foe? | 2018 | VLDB | 6.7904541e-05 |
| 5,262 | RAMP-TAO: Layering Atomic Transactions on Facebook's Online TAO Data Store | 2021 | VLDB | 6.2952027e-05 |
| 7,481 | eXtreme Modelling in Practice | 2020 | VLDB | 5.6078973e-05 |
| 8,715 | Efficient Black-box Checking of Snapshot Isolation in Databases | 2023 | VLDB | 5.3777365e-05 |
| 9,857 | NOC-NOC: Towards Performance-optimal Distributed Transactions | 2024 | SIGMOD | 5.2079113e-05 |
| 11,311 | IsoVista: Black-box Checking Database Isolation Guarantees | 2024 | VLDB | 5.093636e-05 |
Previous
Page 1 / 1
Next
Semantically Similar Papers
| # | Overall Rank | Paper | Year | Venue |
|---|---|---|---|---|
| 1 | 8,715 | Efficient Black-box Checking of Snapshot Isolation in Databases | 2023 | VLDB |
| 2 | 11,371 | Allocating Isolation Levels to Transactions in a Multiversion Setting | 2023 | PODS |
| 3 | 11,128 | When View- and Conflict-Robustness Coincide for Multiversion Concurrency Control | 2024 | PODS |
| 4 | 10,893 | Using Read Promotion and Mixed Isolation Levels for Performant Yet Serializable Execution of Transaction Programs | 2025 | VLDB |
| 5 | 5,475 | Verifiable Properties of Database Transactions | 1996 | PODS |
| 6 | 9,955 | Deciding Robustness for Lower SQL Isolation Levels | 2020 | PODS |
| 7 | 245 | Serializable Isolation for Snapshot Databases | 2008 | SIGMOD |
| 8 | 2,646 | Allocating Isolation Levels to Transactions | 2005 | PODS |
| 9 | 11,311 | IsoVista: Black-box Checking Database Isolation Guarantees | 2024 | VLDB |
| 10 | 10,597 | Fast Verification of Strong Database Isolation | 2026 | VLDB |