Synopsis: Formal methods are used to precisely specify and reason about the behaviors of software systems. This course surveys several methods with an emphasis on methods that support reasoning about specifications and designs. Three themes will pervade our survey:

* The style of description afforded by specification languages.
* The role of verification and validation in software development.
* The influence of representation in automating reasoning about specifications.