@COMMENT This file was generated by bib2html.pl version 0.94 @COMMENT written by Patrick Riley @COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia @InProceedings{seshia-memocode18, author = {Sanjit A. Seshia and Pramod Subramanyan}, title = {UCLID5: Integrating Modeling, Verification, Synthesis, and Learning}, booktitle = {Proceedings of the 15th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, month = {October}, year = {2018}, OPTpages = {97--108}, abstract = {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.}, }