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

Lectures by Sanjit A. Seshia at the 2022 SRI Summer School on Formal Techniques.

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]

Applications

The following paper gives more details on the Trusted Abstract Platform model and verification of enclave platforms (trusted execution environments). This is also referenced 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 two 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]

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

FIS and OGIS:

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]

Videos

Lecture Videos for Day 1: June 2, 2022: (Slides for first 2 videos (PDF).

Introduction & Motivation: Verification of Trusted Computing Platforms
Multi-Modal Modeling with UCLID5
A Brief Introduction to UCLID5 (lecture by Federico Mora for EECS 219C @ UC Berkeley)

Lecture Videos for Day 2: June 4, 2022: (Slides for Day 2 lecture (PDF).

Syntax-Guided Synthesis (lecture recorded in EECS 219C @ UC Berkeley)
Verification by Reduction to Synthesis (lecture recorded in EECS 219C @ UC Berkeley)
Formal Inductive Synthesis and Oracle-Guided Inductive Synthesis (lecture recorded in EECS 219C @ UC Berkeley)
Satisfiability and Synthesis Modulo Oracles (talk by Elizabeth Polgreen at VMCAI'22)

Software

Discussion and lab sections 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).

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 available here. (updated for Day 2)

Exercises: