Collaborative Research: SAIL: An Integration of SAT Solver and Inductive Prover

以下是这三个合作提案的摘要。该项目致力于推理技术的理论进步，以改进软件设计。最近在SAT求解器、决策程序设计、决策程序组合框架和归纳推理自动方法方面的进展，为创建比单个技术更强大的推理系统开辟了可能性。该项目的大部分工作是将它们集成到一个称为SAIL （a SAT和感应实验室）的公共工作台中，该工作台可以作为软件和硬件设计的强大工具。SAIL将纳入几种常用理论的决策程序，包括未解释符号上的相等理论、自由构造函数和Presburger算法。此外，将归纳整合到决策过程而不失去自动化的程序将得到支持。通过创建一个名为SatBox的库，将开发一种新的方法来重用SAT技术。SAIL将包括一种基于SatBox的新的灵活模块化方法，将决策过程集成到基于Davis， Putnam， Logemann和Loveland （DPLL）框架的SAT求解器中。理论和实验进展将在结合决策过程和指导简化、决策过程、SAT求解和归纳定理证明之间的相互作用方面取得进展。SAIL的设计和实现将通过将其应用于各种软件设计应用程序来指导。工作的广泛影响是长期的，导致软件质量和软件开发过程的改进。理论和工具有广泛的应用。

Below is the abstract for these three collaborative proposals.This project works toward theoretical advances in reasoning techniques to improve software design. Recent advances in SAT solvers, design of decision procedures, framework for combining decision procedures, and automatic methods for inductive reasoning have opened possibilities for creating reasoning systems that are more powerful than the individual techniques. Most of the work of the project is to integrate them into a common workbench, called SAIL (A SAT and Induction Laboratory), which can serve as a powerful tool for design of software and hardware. SAIL will incorporate decision procedures for several commonly used theories including theories of equality over uninterpreted symbols, free constructors, and Presburger arithmetic. In addition, procedures for integrating induction into decision procedures without losing automation will be supported. A new approach for reuse of SAT techniques by creating a library called SatBox will be developed. SAIL will include a new flexible, modular approach based on SatBox to integrate the decision procedures into a SAT solver based on the Davis, Putnam, Logemann and Loveland (DPLL) framework. Theoretical and experimental advances will be made in the areas of combining decision procedures and for guiding interactions between simplification, decision procedures, SAT solvers, and induction theorem proving. The design and implementation of SAIL will be guided by applying it on varied software design applications. The broader impacts of the work are long-term, leading to improvements in quality of software and software development processes. The theory and tools have broad applications.