22C:181 - Formal Methods in Software Engineering, Spring 2001

General Info.
Course Homepage
About 22C:181
Contacting Us

Homework & Grades
Grading Policies
Old Homework Directory
Old Exams

Q & A
Meeting outlines

FM Links
Department Homepage
U. of Iowa Homepage

Valid HTML 4.0!
Valid CSS!

Course Syllabus

The table below gives the planned syllabus for the course. This syllabus is subject to change. If it becomes necessary to revise the schedule, then this page will be updated to reflect the changes.

The references in the readings are given in the bibliography below.

Dates Topics Readings Optional Readings
Jan. 16 Introduction Handouts, Course Web Site  
Jan. 16-Feb. 1 Overview of Formal Methods [Wing90] [Hinchey-Bowen95], Formal Methods Virtual Library
Jan. 18 Guest Matt Wilding talks about "Executable Formal models"    
Jan. 25 Guest Steve Miller talks about formal methods at Rockwell    
Feb. 1-Feb. 8 Calculation and Precision [Cohen90] Ch. 0, 1 [Dijkstra76] [Gries91]
Feb. 8-Feb. 20 Predicates [Cohen90] Ch. 2, 3 [Dijkstra-Scholten90]
Feb. 22-Feb. 27 Program Development [Cohen90] Ch. 4-5  
Mar. 1 Exam I [Wing90], [Cohen90] Ch. 1-3 Formal Methods Virtual Library, [Dijkstra-Scholten90] [Dijkstra76]
Mar. 6 Program Development [Cohen90] Ch. 4-5  
Mar. 8 Program Development [Cohen90] Ch. 6-7  
Mar. 13-Mar. 15 Spring Break, no class    
Mar. 22 Program Development [Cohen90] Ch. 6-7  
Mar 27.-Mar. 29 Loops [Cohen90] Ch. 8-9  
Apr. 3 Exam review [Cohen90] Ch. 4-9  
Apr. 5 Exam II [Cohen90] Ch. 4-9  
Apr. 10, Apr. 17 Loops [Cohen90] Ch. 10  
Apr. 12 Recursion [Cohen90] Ch. 11  
Apr. 12, Apr. 19-Apr. 24 JML Intro. [Leavens-Baker-Ruby01] JML web page, [Cohen90] Ch. 12
Apr. 26-May 3 Data Abstraction [Hoare72] [Liskov01] Ch. 5
May 3 Summary and Evaluation    
Tues., May 8, 7-9 p.m. Final Exam [Cohen90] Ch. 10-12, [Leavens-Baker-Ruby01] JML web page, [Liskov01] Ch. 5

Return to top


Edward Cohen. Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, New York, N.Y., 1990.
Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and program semantics. Springer-Verlag, New York, N.Y., 1990.
Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.
Michael G. Hinchey and Jonathan P. Bowen. Applications of Formal Methods FAQ. In Michael G. Hinchey and Jonathan P. Bowen (eds.), Applications of Formal Methods, pp. 1-15, Prentice Hall, London, 1995.
C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271-281 (1972).
David Gries. Teaching Calculation and Discrimination: A More Effective Curriculum. Comm. ACM, 34(3):44-55 (March, 1991).
Gary T. Leavens, and Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Iowa State University, Department of Computer Science, TR98-06n, June 1998, revised July, November 1998, January, April, June, July, August, December 1999, February, May, July, December 2000, February, April 2001. [Postscript] [PDF]
Barbara Liskov with John Guttag. Program Development in Java. Addison-Wesley, Boston, Mass, 2001.
Jeannette M. Wing. A Specifier's Introduction to Formal Methods. Computer, 23(9):8-24 (Sept. 1990).

Return to top

Course Content and Policies

The course's content and grading polices are described on separate web pages. See the links on the top left of this page.

Return to top

Last modified Tuesday, May 8, 2001.

This web page is for the Spring 2001 offering of 22C:181 at the University of Iowa. The details of this course are subject to change as experience dictates. You will be informed of any changes. Thanks to Curt Clifton for help with an earlier version of these web pages. Please direct any comments or questions to Gary Leavens.