Course Description

Formal methods are used to precisely specify and reason about various aspects of software systems. They find a variety of uses at different stages in the software lifecycle, e.g., during conceptual analysis and specification, design, and verification. At the end of this course, you should be able to:

  • understand and use design-by-contract for documentation and for proving a program is correct
  • create analytical models of software designs and use simulation/model-checking techniques to analyze these models
  • use formal notations and proof to specify and refine software requirements
  • exploit formalism to help organize and write specification documents, even if the resulting documents contain no formalism
In addition, you will gain an appreciation for the complexity of design and verification of software systems and the ways in which formal methods can be applied to ameliorate this complexity.

Lectures: 305 Bessey, Mon & Wed 3:00 - 4:20 p.m. with several makeup lectures to be scheduled in advance.

Instructor: Dr. Laura Dillon
Office Hours: 3132 EB, Mon & Wed noon-1:00 p.m., and by appt.
Email: ldillon@cse.msu.edu
Phone: 517-353-4387

Other links