CMSC 630 --- Foundations of Software Verification

Spring 2010




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.




Rance Cleaveland (rance “at” cs dot umd dot edu)
4169 AV Williams Building
Office Hours: Tu 10:45 – 11:45, Th 3:30 – 4:30

Time / Place:

9:30-10:45 TuTh, CSIC 2118


No required text; notes and suggested readings will be made available during the class.


Here is what the workload will be like, together with the impact on your final grade.

  1. Homework assignments (4 - 6)           20%
  2. Midterm                                              20%
  3. Final project                                        30%
  4. Final exam                                           30%


Here also is a tentative lecture schedule for the semester.

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 2-3 research papers covering a particular topic in verification and validation.

Projects are group efforts, with teams consisting of 2-3 people, depending on course enrollment.