UMD logo

CMSC 630: Theory of Programming Languages

Class News
Basic Information

Course goal

The purpose of CMSC 630 is to introduce practical topics related to formal methods for producing software. The structure of the course is:

Basic topics:

Class details:

Class meets: Tues-Thurs 9:05-10:45am, CSIC 3118
Because of the longer class time, on selected dates there will be no class

Instructor: Prof. Marvin Zelkowitz

Office: AVW 4121

Contact: marv@zelkowitz.com (best way)

Grading Criteria

  --Midterm (Date:October 30, 2003)30%
  --Final40%
  --Paper (Date: November 13, 2003)20%
  --Project (Date: December 14, 2003, midnight)10%
Projects

Both a paper and a project will be required.

Problems
Schedule

No textbook is required. Various readings will be distributed in class or available through this web page. For references from easily accessible journals (e.g., Communications of the ACM, IEEE Software, IEEE Computer, IEEE Transactions on Software Engineering) you are expected to obtain your own copy.

DateTopicsReferences
   Basic text for first few weeks = Gannon, Purtilo, Zelkowitz 1994 text on formal methods
September 2-4 Validation of new software engineering methods; Software engineering technology transfer
Slides
"Experimental validation in software engineering" by Marvin V. Zelkowitz and Dolores Wallace" Information and Software Technology (November, 1997) 734-744 (pdf).
"Software Engineering technology infusion within NASA," by M. V. Zelkowitz, IEEE Trans. on Eng. Mgmt. 43, 3 (August, 1996) 250-261 (pdf).
A. Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990
September 9-11 Classical formal methods: Axiomatic verification, weakest precondition "The role of verification in the software specification process," by M. Zelkowitz, Advances in Computers 36, Academic Press (1993) 43-109 (pdf).
C. A. R. Hoare, "An Axiomatic Basic for Computer Programming," Communications of the ACM, Vol. 12, No. 10, 1969, pp. 576-580, 583. (This is the seminal paper on this topic)
Notes on axiomatic proofs (pdf)
Slides on predicate transforms (pdf)
September 16-18 Algebraic data types Notes on algrebraic data types (pdf)
September 23 Functional verification See Advances in Computers article
September 25Denotational semantics See Advances in Computers article
September 30-October 2No Class this week 
October 7-9Z Z Manual by J. M. Spivey
October 14-16PVS PVS Tutorial; PVS User Guide FAQ about Larch
Larch Technical Report
Larch/C++ report
October 21-October 23 Cleanroom, Case studies "Cleanroom Software Engineering" by H. D. Mills, M. Dyer, and R. C. Linger, IEEE Software (September, 1987) 19-25.
Case studies: Ariane 5, Therac 25, NASA MPO and MCL
Ariane 5 failure
Quicktime video of Ariane 5
October 28Midterm review  
October 30Midterm  
November 4Boyer Moore Theorem prover Introduction to BM
Overview paper
November 6No class Candidate for cancelling
November 11 Temporal logic Pages 223-230, 1994 text
November 13Model checking NASA SPIN example
SPIN paper
Alloy - Dan Jackson
Alloy Manual
November 18Lightweight formal methods M. Heimdahl and N. E. Leveson, Completeness and consistency in hierarchical state-based requirements, Transactions on Software Engineering, (22)6, June, 1996, 363-377.
E. Clarke, J. M. Wing, Formal methods: State of the art and future directions
S. Easterbrook, R.R. Lutz, R. Covington, J.C. Kelly, Y. Ampo, and D. Hamilton. Experiences Using Lightweight Formal Methods for Requirements Modeling. IEEE Transaction on Software Engineering, January 1998.
November 20Automatically generated test cases  
November 25No class Candidate for cancelling
November 27No class Thanksgiving Holiday
December 2Practical Formal Methods Research  
December 4 Class reports  
December 9Final Exam  
December 11 No class Candidate for cancelling


Prepared by: Marvin Zelkowitz