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

CRII：SHF：软件开发中可扩展综合的高效 SMT 程序

• 批准号: 1656926
• 负责人: Andrew Reynolds
• 金额: $ 17.49万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-03-01 至 2020-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1656926&HistoricalAwards=false
• 关键词: CRII; SHF; Efficient; SMT; Procedures

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.

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