CSCI3393 · Computer Science
Morrissey College of Arts & Sciences
Complex programs often have bugs, sometimes with serious consequences. Although testing can help root them out, it is impossible to test all possible behaviors of complex programs. To complement testing, one can construct mathematical proofs that programs are correct. This technique, called formal verification, can be done using a tool for writing and automatically checking such proofs. This course introduces formal verification with one such proof checking system called Coq. Students will write precise specifications of how programs should behave, and then carry out proofs in Coq showing that those specifications are met.
Course experience
Averages use the original five-point historical evaluation scale.
Organization
3.7 / 5
How well the course was organized
Challenge
4.5 / 5
How intellectually challenging students found it
Attendance
3.8 / 5
How necessary attendance was
Assignments
4.5 / 5
How helpful assignments were
Weekly effort
~6
hours per week
Estimated from the original workload response buckets. Individual sections may differ.
Instructor options
Ratings below reflect only recovered evaluations connected to this course.
Across time
Section-level results available in the recovered archive.
Spring 2025
1 sectionSpring 2024
1 section