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.
Written reviews 0
No written reviews yet
Numerical ratings and written feedback are separate. Be the first to share what you wish you’d known before taking this course.