tchajed/goose-experiments
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
No description
45 commits 3 branches 0 tags 511 KiB
  • Rocq Prover 96%
  • Go 3.1%
  • Verilog 0.4%
  • Dafny 0.2%
  • Makefile 0.2%
  • Other 0.1%
Find a file
Exact
George Chen 4ff14f2110
 Almost complete proof of wp_mapIter and complete proof of 
wp_MapDeepEqual
2025-12-03 05:00:54 -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 Initial work on map iteration 2025-11-26 03:37:11 -06:00
perennial@e36a12560d Bump Perennial again 2025-11-12 11:09:21 -06:00
src Almost complete proof of wp_mapIter and complete proof of 2025-12-03 05:00:54 -06:00
.gitignore Ignore temporary Vim files 2025-10-12 21:49:54 -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 Automatically compile iterator-related files 2025-10-12 21:50:09 -05:00
README.md Initial version 2025-08-30 10:27:21 -05:00

README.md

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.