UCLID5: Integrating Modeling, Verification, Synthesis and Learning
Sanjit A. Seshia, Pramod Subramanyan · 2018
Formal methods for system design are facing a confluence of transformative trends. First, systems are increasingly heterogeneous, comprising some combination of hardware, software, networking, and physical processes. Second, these systems are increasingly being designed with data-driven methods, in addition to traditional model-based design techniques. Third, traditional automated reasoning techniques based on deduction are being combined with new techniques for inductive inference and machine learning. In this paper, we present UCLID5, a new system for formal modeling, verification, and synthesis that addresses the challenges and opportunities arising from this confluence. UCLID5 can model heterogeneous computational systems, provides term-level abstraction supported by satisfiability modulo theories (SMT) solvers, enables compositional reasoning, and implements the paradigm of verification by reduction to synthesis, leveraging the advances in algorithmic synthesis and machine learning. We describe the key features of UCLID5 using illustrative examples.