Sanjit Seshia, University of California at Berkeley
UCLID5: Integrating Modeling, Verification, Synthesis and Learning


Formal methods for system design are facing a confluence of two intriguing trends. On the one hand, systems are increasingly being designed with data-driven methods, in addition to traditional model-based design techniques. On the other hand, traditional automated reasoning techniques based on deduction are being combined with new techniques for inductive inference and machine learning. In this talk, I will present UCLID5, a new system for formal modeling, verification, and synthesis that addresses the challenges and opportunities arising from this confluence. UCLID5 permits modeling heterogeneous hardware-software systems, provides term-level abstraction and corresponding back-end solvers, supports compositional reasoning, and supports the paradigm of verification by reduction to synthesis, leveraging the advances in algorithmic synthesis and machine learning. As an illustrative application, we will discuss the modeling and verification of trusted hardware-software platforms.