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

Stanford University, Stanford CA

Investigators

Abstract

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.