Formal Methods of Software Engineering
Thursday, 5:00-7:00 PM
Room 1302, Warren Weaver Hall
Amir Pnueli and
- phone: (212) 998-3225
- office: 715 Broadway, Room 707
- office hours: Wednesday 2:00-4:00 PM, or by appointment
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
- phone: (212) 998-3498
- office: WWH 511
- office hours: Wednesday 2:00-7:00 PM, or by appointment
Assignments and a
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.
State of the art approaches to Safety Critical
Systems, as illustrated by the SPARK Ada
A partial survey of formal methods for the specification and
verification of reactive and real-time systems.
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:
- Safety Critical Systems standards.
- Formal testing.
- Report of the WG9 working group on safety critical software.
- Introduction to SPARK Ada.
- A small fully worked out example.
- A survey of formal methods used in industry: Hood, Mascot, etc.
- A computational model for reactive systems.
- Specification language: Temporal Logic.
- Verification methods for sequential programs: Assertional
invariants and variants.
- Model checking of finite-state systems: explicit state and
- Deductive verification.
- Scaling up: Abstraction and (De)Composition.
- High Integrity Ada, The Spark Approach. John Barnes, Addison
- Systems and Software Verification: Model-Checking Techniques and
Tools. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit,
L. Petrucci, and P. Schnoebelen, Springer.
Lecture 0 -- Sept. 6, 2001:
Building Reliable Software.ppt,
Formal - L0.ps,
Lecture 1 -- Sept. 20, 2001:
Formal - L1.ps,
Lecture 2 -- Sept. 27, 2001:
Formal - L2.ps,
Lecture 3 -- Oct.    4, 2001:
Formal - L3.ps,
Lecture 4 -- Oct.   11, 2001:
Formal - L4.ps,
Lecture 5 -- Oct.   25, 2001:
Formal - L5.ps,
Introduction to Spark and Tutorial:
Lecture 6 -- Nov.   1, 2001:
Formal - L6.ps,
Lecture 7 -- Nov.   8, 2001:
Formal - L7.ps,
Lecture 8 -- Nov.  15, 2001:
Formal - L8.ps,