Formal Methods of Software Engineering

Thursday, 5:00-7:00 PM
Room 1302, Warren Weaver Hall
Amir Pnueli
and Robert Dewar

Reaching Us

Amir Pnueli

Robert Dewar

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and parallel programs.

Course requirements: Assignments and a term project.

Course Description

Software Engineering is a collection of techniques which enable programmers and system designers to construct large software systems in a systematic, effective, and reliable manner. They are particularly useful for projects which involve large teams of designers/programmers, and absolutely essential for systems which are identified as safety critical, i.e., systems where a single failure may result in loss of human life. The Formal Methods approach to software construction is based on viewing a program and its execution as mathematical objects and applying mathematical and logical techniques to specify and analyze the properties and behavior of these objects. The main advantages of the formal approach to software construction is that, whenever applicable, it can lead to an increase of the reliability and correctness of the resulting programs by several orders of magnitude. Again, the main potential beneficiary of such an increase is the class of safety critical systems. This course consists of two mutually supportive components: Of particular importance will be the links between the two components, where part 1 will identify the need and motivation for formal methods and part 2 will identify the available solutions to these needs.

A partial list of the topics to be covered within part 1 is: A partial list of the topics to be covered within part 2 is:

Recommended Texts

Class Presentations


TLV Resources