Program Verification and Synthesis for Migrating Database Applications

数据库应用程序在当今的软件基础设施中无处不在，在现代社会的许多方面发挥着重要作用。各种新兴的数据库系统（如Redis、MongoDB、Neo4j）和云数据库服务（如Amazon DynamoDB）为迁移数据库应用程序带来了新的挑战。该研究项目旨在开发新的编程语言技术和工具，以促进数据库应用程序的正确、自动化和最佳迁移。1. 的正确性。为了确保迁移过程的正确性，开发人员需要验证迁移后的数据库应用程序是否等同于或改进了原始版本。受此问题的启发，本研究计划提出了新的验证技术，用于检查关系和非关系数据库上数据库应用程序的等价性和精化。2. 自动化。由于迁移数据库应用程序需要大量的手工工作，因此迫切需要自动化迁移过程。本研究项目提出了一种新的程序合成技术，可以在关系数据库、面向文档数据库和图形数据库上自动生成应用程序。这种综合技术可以显著减少迁移过程中涉及的手工工作，从而提高开发人员的工作效率。3. 最优。随着各种数据库的激增，选择合适的高性能数据模型变得越来越具有挑战性，因为需要在关系、JSON文档、图及其组合之间进行权衡。本研究提出了一种定量合成技术，可以根据给定的工作量生成最优的数据模型，并根据该模型自动合成最优的数据库应用程序。定量综合技术可以简化数据建模过程，帮助开发人员在最优的数据模型上获得最佳的数据库应用程序。本研究计划探索在不同数据库上迁移数据库应用程序的编程语言技术。它有可能开辟一个将程序设计语言研究和数据库研究相结合的新的研究领域，可以激励更多的研究人员在这两个领域做出创新的科学贡献。此外，它还为培养几名计算机科学博士和硕士研究生提供了良好的机会，帮助他们学习前沿技术，建立编程语言和数据库的研究技能。最后，本研究计划中提出的技术和工具可以潜在地使加拿大公司和组织广泛受益，这些公司和组织利用数据库应用程序来管理其日常操作或向公众提供服务。

Database applications are ubiquitous in today's software infrastructure and play important roles in many aspects of modern society. Various emerging database systems (e.g., Redis, MongoDB, Neo4j) and cloud database services (e.g., Amazon DynamoDB) bring new challenges for migrating database applications. This research program aims to develop new programming language techniques and tools that facilitate correct, automated, and optimal migrations of database applications. 1. Correctness. To ensure the correctness of the migration process, developers need to verify the database application after the migration is equivalent to, or refinement of, the original version. Motivated by this problem, this research program proposes new verification techniques for checking equivalence and refinement of database applications over relational and non-relational databases. 2. Automation. Since migrating database applications requires lots of manual effort, there is a pressing demand for automating the migration process. This research program presents a novel program synthesis technique that can automatically generate an application over relational, document-oriented, and graph databases. This synthesis technique can significantly reduce the manual effort involved in the migration process and thus improve developer productivity. 3. Optimality. With the proliferation of various kinds of databases, selecting a suitable and performant data model is increasingly challenging because of the trade-offs in relations, JSON documents, graphs, and their combinations. This research proposes a quantitative synthesis technique that can generate an optimal data model based on a given workload and automatically synthesize an optimal database application based on the model. The quantitative synthesis technique can simplify the data modeling procedure and help developers obtain the best database application over an optimal data model. This research program explores programming language techniques for migrating database applications over various databases. It has the potential to open up a new research area that combines programming language research and database research, which can inspire more researchers to make innovative scientific contributions in both fields. In addition, it provides good opportunities to train several PhD and master students in computer science and help them learn cutting-edge technologies and build research skills in programming languages and databases. Finally, the techniques and tools proposed in this research program can potentially benefit a broad spectrum of Canadian companies and organizations that leverage database applications to manage their daily operations or provide services to the public.