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

University Of Iowa, Iowa City IA

Investigators

Abstract

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.