Program proofs for Systems Verification Fall 2025 at UW-Madison
  • Rocq Prover 96.5%
  • Go 2.7%
  • Verilog 0.3%
  • Dafny 0.2%
  • Makefile 0.2%
  • Other 0.1%
Find a file
2025-11-19 18:45:08 -06:00
.devcontainer Bump docker image version 2025-08-30 11:20:24 -05:00
.vscode Initial version 2025-08-30 10:27:21 -05:00
dafny Initial version 2025-08-30 10:27:21 -05:00
etc Initial version 2025-08-30 10:27:21 -05:00
go Release revised HW4 2025-11-19 18:45:08 -06:00
perennial@7a19a5cc18 Upgrade perennial 2025-11-03 07:53:11 -06:00
src Release revised HW4 2025-11-19 18:45:08 -06:00
.gitignore Initial version 2025-08-30 10:27:21 -05:00
.gitmodules Initial version 2025-08-30 10:27:21 -05:00
_CoqProject Initial version 2025-08-30 10:27:21 -05:00
Makefile Initial version 2025-08-30 10:27:21 -05:00
README.md Initial version 2025-08-30 10:27:21 -05:00

Systems verification assignments

These are the proof assignments for CS 839: Systems verification, taught at UW-Madison in Fall 2025 by Tej Chajed.

Please don't fork the repo since it will make your solutions public. Follow the setup instructions on the course website. The instructions also describe how to set up Coq.

Once you have Coq installed, build the provided code by running make.

Getting updates

You'll need to use git pull to get updates and new assignments.