Course materials for Systems Verification at UW-Madison
- Rocq Prover 91%
- Rust 5.6%
- Go 2.5%
- Verilog 0.3%
- Shell 0.3%
- Other 0.3%
|
|
||
|---|---|---|
| .devcontainer | ||
| .github | ||
| .vscode | ||
| dafny | ||
| etc | ||
| go | ||
| src | ||
| template | ||
| .editorconfig | ||
| .gitignore | ||
| .gitignore-student | ||
| .gitmodules | ||
| _RocqProject | ||
| fix.txt | ||
| LICENSE | ||
| Makefile | ||
| README-student.md | ||
| README.md | ||
| sys-verif.opam | ||
Systems Verification materials
go/: code to be verifiedsrc/: all Rocq proofssoftware_foundations/: exercise files from Logical Foundations chapter of SFsys_verif/: literate course notes and demosGoose/: generated code from goose
template/: tooling for compiling assignments, demos, and lecture notesetc/some scripts for managing this repo itself
The root directory has the Rocq setup (Makefile, sys-verif.opam,
_RocqProject) and VS Code setup (.devcontainer, .vscode).
Updating things
./etc/template repo ../sys-verif-fa26-proofs
./etc/template web ../sys-verif-fa26
Update the Software Foundations exercises distributed in src/software_foundations:
./etc/update-lf.sh
Including solutions
Assuming the private solutions repo is checked out adjacent to this repo:
ln -s $(realpath ../sys-verif-solutions/src/sys_verif/assignment_solns) src/sys_verif/
Testing
make
cd template
cargo test
cd go
go test ./...
cd dafny
dafny verify *.dfy
dafny format --check *.dfy