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 (accepted pending artifact evalution). 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),
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.
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:
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)