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

该项目扩展了可满足性模理论(SMT)求解器，使其具有对软件综合应用非常重要的功能。PI主要集中于为感兴趣的已知逻辑片段开发合成过程，包括具有一个量词交替的固定宽度位向量公式，其中现有SMT解算器的支持是有限的。此外，该项目还开发了SMT解算器中的功能，以满足新领域中新出现的合成问题的需要。这包括支持新的背景理论，如有界字符串理论，以及处理当前算法不能很好扩展的一类合成问题的新方法。作为该项目的一部分，PI扩展了SMT解算器和合成应用程序之间的通信接口，包括支持部分解和合成猜想的反例。该项目包括与SMT解算器的外部用户合作，这些用户提供了激励这项工作的具有挑战性的问题。PI们希望该项目不仅有助于SMT求解的最先进水平，还有助于其他推理工具，如依赖不变合成的高阶定理证明器和模型检查器。

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.