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 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 and requirements documents that are clear and precise
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: 313 Bessey, Mon & Wed 10:20 - 11:40 a.m. with a few exceptions noted on the schedule.

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

Other links