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).
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):
To build and use a Docker image, please clone the following github repository and follow the instructions:
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.
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.
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]
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.
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.
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),
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.
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,
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
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.
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,
Susmit Jha and Sanjit A. Seshia. A Theory of Formal Synthesis via Inductive Learning. Acta Informatica,
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.