eXtreme Modelling in Practice
Summary: TLA+-based modelling of MongoDB subsystems to verify spec–implementation conformance. Case studies: MBTC on Server replication vs MBTCG on Realm Sync OT; MBTC fails for abstract specs, MBTCG succeeds, guiding future MBT in data management. (summarized by gpt-5-nano on Feb 09 2026)
Incoming Non-self Citations Over Time
Authors
Incoming Citations (Sorted by Pagerank)
Showing 2 of 2 citing papers.
| Rank | Citing Paper | Year | Venue | Pagerank |
|---|---|---|---|---|
| 10,549 | VerIso: Verifiable Isolation Guarantees for Database Transactions | 2025 | VLDB | 4.1945683e-05 |
| 10,781 | Design and Modular Verification of Distributed Transactions in MongoDB | 2025 | VLDB | 4.1945683e-05 |
Previous
Page 1 / 1
Next
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 |
|---|---|---|---|---|
| 3,672 | Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB | 2019 | SIGMOD | 6.8558714e-05 |
| 4,347 | Tunable Consistency in MongoDB | 2019 | VLDB | 6.269146e-05 |
| 6,636 | Adapting TPC-C Benchmark to Measure Performance of Multi-Document Transactions in MongoDB | 2019 | VLDB | 4.9820843e-05 |
Previous
Page 1 / 1
Next