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.