Collaborative Research: SHF: Small: Integrating Synthesis and Optimization in Satisfiability Modulo Theories

合作研究：SHF：小型：在可满足性模理论中集成综合和优化

• 批准号: 2006407
• 负责人: Clark Barrett
• 金额: $ 25万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-06-01 至 2023-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2006407&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Small; Integrating

The ever-increasing demand for optimized large-scale computing systems puts pressure on attaining significant improvements in automated design optimization and synthesis tools. This project aims to overcome the limitations of prior approaches through a tighter integration of optimization and synthesis algorithms leveraging advances in modern automated reasoning systems. The project demonstrates the power of Satisfiability Modulo Theories (SMT)-based synthesis combined with emerging research in Optimization Modulo Theories (OMT). The project explores advances in both theory and practice, with research demonstrations integrated into CVC4, the only SMT solver today providing synthesis features. In particular, CVC4 is being extended with optimization capabilities, making it the first automated reasoning tool capable of performing synthesis and optimization together. The resulting extensible framework enables system design for emerging technologies which often require reasoning over non Boolean (and mixed) primitives. The extensibility and generality of the approach charts a new direction of research at the intersection of synthesis and optimization, leads towards more scalable and complex system design, and allows optimization over a broader class of objectives including security and safety.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

对优化的大规模计算系统的不断增长的需求对自动化设计优化和综合工具的重大改进施加了压力。该项目旨在利用现代自动推理系统的进步，通过优化和综合算法的更紧密集成来克服现有方法的局限性。 该项目展示了基于可满足性模理论（SMT）的合成与优化模理论（OMT）的新兴研究相结合的力量。该项目探索了理论和实践方面的进展，并将研究演示集成到CVC 4中，CVC 4是当今唯一提供合成功能的SMT求解器。 特别是，CVC 4正在扩展优化功能，使其成为第一个能够同时执行合成和优化的自动推理工具。由此产生的可扩展框架，使系统设计的新兴技术，往往需要推理非布尔（和混合）原语。该方法的可扩展性和通用性为综合和优化的交叉点开辟了一个新的研究方向，导致了更可扩展和更复杂的系统设计，并允许对更广泛的目标进行优化，包括安全性和安全性。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

项目成果

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery

通过匹配和重写规则发现进行 SyGuS 解决方案拟合的过程

• 发表时间: 2023
• 期刊: Proceedings of the 23rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23
• 作者: Mohamed, Abdalrhman;Reynolds, Andrew;Barrett, Clark;Tinelli, Cesare
• 通讯作者: Tinelli, Cesare

Automating System Configuration

自动化系统配置

• DOI: 10.34727/2021/isbn.978-3-85448-046-4_19
• 发表时间: 2021
• 期刊: Proceedings of the 21st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21
• 作者: Tsiskaridze, Nestan;Strange, Maxwell;Mann, Makai;Sreedhar, Kavya;Liu, Qiaoyi;Horowitz, Mark;Barrett, Clark
• 通讯作者: Barrett, Clark

Temporal Computing With Superconductors

• DOI: 10.1109/mm.2021.3066377
• 发表时间: 2021-05-01
• 期刊: IEEE MICRO
• 影响因子: 3.6
• 作者: Tzimpragos, Georgios;Volk, Jennifer;Sherwood, Timothy
• 通讯作者: Sherwood, Timothy