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

合作研究：SAIL：SAT 求解器和归纳证明器的集成

• 批准号: 0541057
• 负责人: Mahadevan Subramaniam
• 金额: $ 8万
• 依托单位: University of Nebraska at Omaha
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-09-15 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541057&HistoricalAwards=false
• 关键词: Collaborative; Research; SAIL; Integration; SAT

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.

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