Verification of Database-driven Systems via Amalgamation
Summary: Framework for static verification of finite-register, database-driven systems whose transitions are quantifier-free queries over a fixed constrained database (data trees or relations). Technique based on amalgamation yields ExpSpace decidability for XML data trees with descendant and data comparisons, PSpace for relational schemas, and shows slight model extensions are undecidable. (summarized by gpt-5-mini on Feb 09 2026)
Incoming Non-self Citations Over Time
Authors
- 1. Mikołaj Bojańczyk (University of Warsaw)
- 2. Luc Segoufin (INRIA; École Normale Supérieure)
- 3. Szymon Toruńczyk (University of Warsaw)
BibTeX Citation
@inproceedings{bojanczyk_pods13,
address = {New York, NY, USA},
series = {{PODS} '13},
title = {{Verification of Database-driven Systems via Amalgamation}},
url = {https://dl.acm.org/doi/10.1145/2463664.2465228},
doi = {10.1145/2463664.2465228},
booktitle = {Proceedings of the {ACM} {SIGMOD} Symposium on {Principles} of {Database} {Systems}},
publisher = {Association for Computing Machinery},
author = {Bojańczyk, Mikołaj and Segoufin, Luc and Toruńczyk, Szymon},
year = {2013}
}
Incoming Citations (Sorted by Pagerank)
Showing 3 of 3 citing papers.
| Rank | Citing Paper | Year | Venue | Pagerank |
|---|---|---|---|---|
| 5,959 | Recency-Bounded Verification of Dynamic Database-Driven Systems | 2016 | PODS | 6.0274692e-05 |
| 11,752 | Projection Views of Register Automata | 2020 | PODS | 5.093636e-05 |
| 11,839 | Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding | 2019 | PODS | 5.093636e-05 |
Previous
Page 1 / 1
Next
Outgoing Citations (Sorted by Pagerank)
Showing 1 of 1 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,826 | A System for Specification and Verification of Interactive, Data-driven Web Applications | 2006 | SIGMOD | 7.0916124e-05 |
Previous
Page 1 / 1
Next
Semantically Similar Papers
| # | Overall Rank | Paper | Year | Venue |
|---|---|---|---|---|
| 1 | 874 | On the Decidability and Complexity of Query Answering over Inconsistent and Incomplete Databases | 2003 | PODS |
| 2 | 4,659 | On The Complexity And Axiomatizability Of Consistent Database States | 1984 | PODS |
| 3 | 1,630 | On the Decidability of Query Containment under Constraints | 1998 | PODS |
| 4 | 3,781 | A Modal System of Algebras for Database Specification and Query/Update Language Support | 1983 | VLDB |
| 5 | 3,679 | XML with Data Values: Typechecking Revisited | 2001 | PODS |
| 6 | 12,410 | Certain Answers for XML Queries | 2010 | PODS |
| 7 | 5,959 | Recency-Bounded Verification of Dynamic Database-Driven Systems | 2016 | PODS |
| 8 | 5,874 | Verification of Relational Data-Centric Dynamic Systems with External Services | 2013 | PODS |
| 9 | 12,351 | Querying Schemas With Access Restrictions | 2012 | VLDB |
| 10 | 11,839 | Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding | 2019 | PODS |