
CMSC 630  Foundations of Software Verification Spring 2010

Overview: 
This course is about the principles of software verification: the theory and practice of systematically reasoning about the correctness of software. In the class you will learn different techniques for writing down precise specifications of desired system behavior (“preconditions / postconditions”, “temporal logic”, “process algebra”) and for proving that specifications indeed hold of software. You will also learn about algorithmic approaches (“model checking”) for automatically establishing such correctness results. 
Instructor: 
Rance Cleaveland (rance
“at” cs dot umd dot edu) 
Time / Place: 
9:3010:45 TuTh, CSIC 2118 
Text: 
No required text; notes and suggested readings will be made available during the class. 
Coursework: 
Here is what the workload will be like, together with the impact on your final grade.

Final Project: 
The course does have a final project, which will take one of two forms. In the first, you will specify and verify a system of your choice either by hand (i.e., on paper using one of the formal techniques discussed in class) or with the aid of one or more verification tools, and give a presentation in class summarizing your efforts. In the second, you will present a lecture summarizing the research findings contained in 23 research papers covering a particular topic in verification and validation. Projects are group efforts, with teams consisting of 23 people, depending on course enrollment. 