CAREER: Generating Provably Correct Query Optimizers

数据库查询优化器是大型、复杂且容易出错的软件系统。这个项目的目标是帮助研究人员和开发人员构建“可证明是正确的”优化器。具体地说，该研究小组正在构建一个框架，该框架接受优化器组件及其交互的规范，并生成优化器，这些优化器可以显示为满足这样一个特性，即它们构建的计划总是返回用户查询中指定的数据。该小组的方法将优化器的组件分为需要正确性证明的组件(安全关键组件)和不需要正确性证明的组件。语言正在设计中，用于正式指定这些组件，工具正在构建中，这些工具既根据规范生成这些组件，又生成证明义务，使它们能够使用自动定理证明器进行验证。实验研究与培训学生在构建大型软件系统中应用形式化方法的教育目标相联系。该项目的成果将为学术界和工业界的数据库研究人员提供一个沙箱，以引入新的优化器技术和产品，同时提供没有错误的切实保证。{http://www.cs.brandeis.edu/~mfc/cokokola.html}

Database query optimizers are large, complex, and error-prone software systems. The goal of this project is to assist researchers and developers in building optimizers that are "provably correct". Specifically, this research group is building a framework which accepts specifications of optimizer components and their interactions, and generates optimizers that can be shown to satisfy the property that the plans they construct always return the data specified in a user queries. The group's approach separates the components of the optimizer into those that require correctness proofs (the safety critical components) from those that do not. Languages are under design for formally specifying those components, and tools are under construction that both generate these components according to the specifications, and generate proof obligations enabling their verification with an automated theorem prover. The experimental research is linked to the educational goal of training students in the application of formal methods in building large software systems. The results of this project will provide a sandbox for database researchers in both academia and industry, to introduce new optimizer techniques and products while providing tangible guarantees that they are free of errors. {http://www.cs.brandeis.edu/~mfc/cokokola.html}