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.

Detailed Award Information

Award Information:
Title: Collaborative Research: SHF: Small: Integrating Synthesis and Optimization in Satisfiability Modulo Theories
ID: 2006407
Effective Date: 06/01/2020
Expiration Date: 05/31/2023
Amount: $250,000

Institution Information:
Name: Stanford University
City: Palo Alto
State: CA
Country: United States
MSI: Other Institution

Investigator Information:
Role Code: Principal Investigator
Name: Clark Barrett
Email Address:

Organization Information:
Directorate: 4900
Division: NSF

Program Information:
Code: 4900
Text: Software & Hardware Foundation