Fall 2004

Upon completion of this course, you will be familiar with the scope and limits of formal verification, including the role of semantics, major specification approaches, and feasibile automated support. You will be familiar with rules for proving correctness of sequential code including loops as well as concurrent programs. You will be skilled in the use of first order predicate logic to specify structural models of software including invariants and operation transitions. You will be skilled in the use of the Alloy tool for checking such specifications and generating test examples from them. You will be skilled in the use of the ESC/Java-2 tool for verification of method implementations with respect to specifications.