Resources
Practical references and tools for CARS. See also:
- Setup for Python and Z3 installation
- Library for 76 curated readings on formal methods and solver-aided programming
- Bibliography for academic references
Accessing Paywalled Readings
Some readings linked from the course are behind publisher paywalls (ACM, IEEE, Springer). As a UW student you have free access to these through the UW Libraries.
Option 1: Off-campus access. Follow the UW Libraries off-campus access instructions to set up proxy access through your browser.
Option 2: Bookmarklet. Install the UW Libraries proxy bookmarklet. When you hit a paywall, click the bookmarklet and log in with your UW NetID to access the article.
Z3
- Z3 Guide — interactive tutorial and examples
- Programming Z3 — comprehensive guide by Nikolaj Bjorner (Z3 co-creator)
- Z3 online playground — run Z3 in the browser (SMT-LIB syntax only)
- Z3 API documentation — Python API reference for Z3Py
- Z3 GitHub repository — source code, issues, releases
SMT-LIB
SMT-LIB is the standard input language for SMT solvers. CARS uses Python and Z3 as the primary interface, but you will encounter SMT-LIB in examples and documentation.
- SMT-LIB standard — the specification language for SMT solvers
- SMT-LIB tutorial (Rise4Fun archive) — walkthrough of Z3 in SMT-LIB format
Rosette
We will use Rosette starting in Week 7.
- Rosette Guide — language reference and tutorial
- Rosette — overview, papers, and course links
- Rosette GitHub — source code and installation
Python
- Python documentation — official reference
- venv documentation — virtual environment setup and usage
Git
- GitHub Git Guide — beginner-friendly overview of core commands
- Install Git — installation for macOS, Windows, and Linux
- Git documentation — official reference
VS Code
- VS Code download — our officially supported editor
- Python extension — required for Python development in VS Code
Related Courses
Courses at other universities covering similar topics:
- Stanford CS 357S — hardware verification with SAT/SMT and model checking
- UT Austin CS 389L — automated logical reasoning with SAT/SMT and Dafny
- CMU 15-414 — bug catching and verification with Why3 and Lean
- UIUC CS 477 — formal software development methods
- UMD CMSC 433 — programming language technologies with Dafny and Z3
- EPFL CS-550 — formal verification with Stainless and Isabelle
- UW CSE 507 — computer-aided reasoning with Rosette and Alloy (the course CARS builds on)