CRII: SHF: Efficient SMT Procedures for Scalable Synthesis in Software Development

University Of Iowa, Iowa City IA

Investigators

Abstract

This project extends Satisfiability Modulo Theories (SMT) solvers with capabilities of importance to software synthesis applications. The PIs focus primarily on developing synthesis procedures for known logical fragments of interest, including fixed-width bit-vector formulas with one quantifier alternation, where support in existing SMT solvers is limited. Additionally, this project develops functionality in SMT solvers to meet the needs of emerging synthesis problems in new domains. This includes support for new background theories such as the theory of bounded strings, and new methods for tackling classes of synthesis problems where current algorithms do not scale well. As part of the project, the PIs expand the communication interface between SMT solvers and synthesis applications, including support for partial solutions and for counterexamples to synthesis conjectures. The project includes collaboration with external users of SMT solvers who provide challenging problems that motivate this work. The PIs expect the project to both contribute to the state-of-the-art in SMT solving, and to benefit other reasoning tools such as higher-order theorem provers and model-checkers that rely on invariant synthesis.