UCLID5's Elements: Formal Modeling, Verification, Synthesis, and Learning

Lectures by Sanjit A. Seshia at the 2022 SRI Summer School on Formal Techniques and the 2022 SAT-SMT Winter School.

   Videos and Slides

Here are the slides for the lectures given at the 2022 SAT-SMT Winter School: Day 1 (PDF), Day 2 (PDF).

Pre-recorded Lecture Videos are also available. These were recorded for the 2022 SRI Summer School on Formal Techniques, and give more details beyond what was covered in the summer/winter school on-site lectures.
Pre-recorded Lecture Videos for Day 1: (Slides for first 2 videos below (PDF).

Pre-recorded Lecture Videos for Day 2: (Slides for Day 2 lecture (PDF).


Discussion and demos/labs in the tutorial will use the following software toolkit (available open-source on github):

UCLID5: A system for modeling, verification, and synthesis of computational systems.

To do the labs, you can clone the above repository and follow instructions to compile on your system. UCLID5 works on Linux, MacOS, and Windows (WSL2). Examples used in the demos/labs are available in the following repository (under uclid_artefact/examples): https://github.com/uclid-org/uclid5-ssft22.

To build and use a Docker image, please clone the following github repository and follow the instructions: https://github.com/uclid-org/uclid5-ssft22.
You will need to have previously installed Docker on your system.

If you are unable to build the Docker image yourself, you may try the pre-built Docker image linked to from the repository above.

   Reading Materials

Start by reading this perspective paper:
Combining Induction, Deduction, and Structure for Verification and Synthesis, Sanjit A. Seshia, Proceedings of the IEEE, 103(11):2036–2051, 2015.

Overview of UCLID5

The following 2 papers give an overview of UCLID5. The first sketches out the motivation for UCLID5 and its early design decisions. The second paper gives an updated summary of the capabilities of UCLID5 circa 2022.

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] 

Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. Proc. Computer-Aided Verification (CAV), August 2022. Download: [pdf] 


The following paper gives more details on the Trusted Abstract Platform model and verification of enclave platforms (trusted execution environments). This is also a case study in the CAV'22 paper referenced above.

Pramod Subramanyan, Rohit Sinha, Ilia A. Lebedev, Srinivas Devadas, and Sanjit A. Seshia. A Formal Foundation for Secure Remote Execution of Enclaves. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2435–2450, 2017.
Download: [pdf] 

Here are some other published applications of UCLID5 (optional reading):

Albert Magyar, David Biancolin, John Koenig, Sanjit A. Seshia, Jonathan Bachrach, and Krste Asanovic. Golden Gate: Bridging The Resource-Efficiency Gap Between ASICs and FPGA Prototypes. In In Proceedings of the International Conference on Computer-Aided Design (ICCAD), pp. 1–8, November 2019.
Download: [HTML] 

Kevin Cheang, Cameron Rasmussen, Sanjit A. Seshia, and Pramod Subramanyan. A Formal Approach to Secure Speculation. In Proceedings of the Computer Security Foundations Symposium (CSF), June 2019.
Download: [pdf] 

Dayeol Lee, Kevin Cheang, Alexander Thomas, Catherine Lu, Pranav Gadamaduggu, Anjo Vahldiek-Oberwagner, Mona Vij, Dawn Song, Sanjit A. Seshia, and Krste Asanovic. Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS), 2022.
Download: [pdf] 

Background References on Formal Modeling

This is an introduction to creating models for formal verification:

Sanjit A. Seshia, Natasha Sharygina, and Stavros Tripakis. Modeling for Verification. In Edmund M. Clarke, Thomas Henzinger, and Helmut Veith, editors, Handbook of Model Checking, Springer, 2014.
Download: [pdf] 

Basics of formal modeling and examples (in the context of embedded/cyber-physical systems) can also be found in this textbook:

Edward A. Lee and Sanjit A. Seshia. Introduction to Embedded Systems: A Cyber-Physical Systems Approach, Second edition, MIT Press, 2017.
Available online: LeeSeshia.org 

Background on SMT Solving and Syntax-Guided Synthesis

SMT Solving:

Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, pp. 1267–1329, IOS Press, 2021. Second edition.
First edition version available here.
Download: [pdf] 

Syntax-Guided Synthesis (SyGuS):

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-Guided Synthesis. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 1–17, October 2013.
Download: [pdf] 

Formal Inductive Synthesis and Oracle-Guided Synthesis


Susmit Jha and Sanjit A. Seshia. A Theory of Formal Synthesis via Inductive Learning. Acta Informatica, 54(7):693–726, 2017.
Download: [pdf] 

Satisfiability and Synthesis Modulo Oracles (SMTO and SyMO):

Elizabeth Polgreen, Andrew Reynolds, and Sanjit A. Seshia. Satisfiability and Synthesis Modulo Oracles. In Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2022.
Download: [pdf]