Fri 12 Jan 2018 14:55 - 15:20 at Bunker Hill - Program Analysis II Chair(s): Isil Dillig

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 Jan

POPL-2018-papers
13:30 - 15:20: Research Papers - Program Analysis II at Bunker Hill
Chair(s): Isil DilligUT Austin
POPL-2018-papers13:30 - 13:40
Awards
Benjamin DelawarePurdue University
POPL-2018-papers13:30 - 13:52
Talk
Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego
POPL-2018-papers14:05 - 14:30
Talk
Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
POPL-2018-papers14:30 - 14:55
Talk
POPL-2018-papers14:55 - 15:20
Talk
Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin