Formal methods for database schema refactoring

Database applications typically undergo several schema refactorings during their life cycle due to performance or maintainability reasons. Such refactorings not only require migrating the underlying data to a new schema but also re-implementing large chunks of the code that query and update the database. The code and data migration tasks implied by schema refactoring are notoriously challenging to developers, as they are time-consuming and error-prone.

Motivated by these challenges, this dissertation presents formal method techniques to help developers correctly and easily evolve database applications during schema refactoring. Specifically, it first describes how to verify equivalence between database applications that operate over different schemas, such as those that arise before and after schema refactoring. Next, it presents a novel technique that can automatically synthesize an equivalent version of the database program that operates over the new schema. Finally, it describes a synthesis technique that helps developers migrate data between schemas using input-output examples.

We also implement research prototypes based on the proposed techniques and perform experiments to evaluate their effectiveness and efficiency. The experimental results demonstrate that our techniques are effective for code and data migration during schema refactoring, and they are more efficient than several baselines and state-of-the-art approaches.