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 and SMT

• Z3 GitHub repository — source code, issues, releases
• Z3 API documentation — Python API reference for Z3Py
• 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)
• SMT-LIB standard — the specification language for SMT solvers
• SMT-LIB tutorial (Rise4Fun archive) — walkthrough of Z3 in SMT-LIB format

Python

• Python documentation — official reference
• venv documentation — virtual environment setup and usage

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)