Verifying Equivalence of Database-Driven Applications
This paper addresses the problem of verifying equivalence between a pair of programs that operate over databases with different schemas. This problem is particularly important in the context of web applications, which typically undergo database refactoring either for performance or maintainability reasons. While the web application should have the same externally observable behavior before and after schema migration, there are no existing tools for proving equivalence of such programs. This paper takes a first step towards solving this problem by formalizing the equivalence and refinement checking problems for database-driven applications. We then propose a proof methodology based on the notion of bisimulation invariants over a new logic called the theory of relational algebra with updates. We also present a fully automated technique for synthesizing such bisimulation invariants and automatically verify their correctness. We have implemented the proposed technique in a tool called Mediator and show that it can verify the equivalence of real-world web applications containing hundreds of transactions.
Fri 12 JanDisplayed time zone: Tijuana, Baja California change
13:30 - 15:20
Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Işil Dillig UT Austin
Benjamin Delaware Purdue University
|Refinement Reflection: Complete Verification with SMT|
Niki Vazou University of Maryland, Anish Tondwalkar UCSD, Vikraman Choudhury , Ryan Scott Indiana University, Ryan R. Newton Indiana University, Philip Wadler University of Edinburgh, UK, Ranjit Jhala University of California, San Diego
|Non-Linear Reasoning For Invariant Synthesis|
Zachary Kincaid Princeton University, John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
|A Practical Construction for Decomposing Numerical Abstract Domains|
Gagandeep Singh , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich
|Verifying Equivalence of Database-Driven Applications|
Yuepeng Wang University of Texas at Austin, Işil Dillig UT Austin, Shuvendu K. Lahiri Microsoft Research, William Cook University of Texas at Austin