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

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

基本信息

批准号：
0541315
负责人：
Deepak Kapur
金额：
$ 14.56万
依托单位：
University of New Mexico
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2006
资助国家：
美国
起止时间：
2006-09-15 至 2009-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541315&HistoricalAwards=false
关键词：
Collaborative Research SAIL Integration SAT

项目摘要

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.

以下是这三个协作提案的摘要。该项目致力于推理技术的理论进步，以改善软件设计。 SAT求解器的最新进展，决策程序的设计，结合决策程序的框架以及用于归纳推理的自动方法，为创建比单个技术更强大的推理系统开辟了可能性。该项目的大部分工作都是将它们集成到一个称为SAIL（SAT和感应实验室）的普通工作台中，该工作台可以用作设计软件和硬件设计的强大工具。 SAIL将纳入几种常用理论，包括对未解释的符号，自由构造函数和前汉堡算术的决策程序。此外，将支持将归纳归纳为决策程序而不会丢失自动化的程序。通过创建称为SATBOX的库来重复使用SAT技术的新方法。 SAIL将包括基于SATBOX的新的灵活的模块化方法，以将决策程序集成到基于Davis，Putnam，Logemann和Loveland（DPLL）框架的SAT求解器中。理论和实验进步将在结合决策程序的领域以及指导简化，决策程序，SAT求解器和归纳定理之间的相互作用的领域进行。帆的设计和实施将通过将其应用于各种软件设计应用程序中进行指导。工作的更广泛影响是长期的，从而改善了软件和软件开发过程的质量。理论和工具具有广泛的应用。