UCLID5: Integrating Modeling, Verification, Synthesis, and Learning

Sanjit A. Seshia and Pramod Subramanyan. UCLID5: Integrating Modeling, Verification, Synthesis, and Learning. In Proceedings of the 15th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), October 2018.

Download

[pdf] 

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.

BibTeX

@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.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Wed May 29, 2019 23:46:23