CMSC 631, Spring 2009

Program Analysis and Understanding

  • Apr 27. Here is a sample solution to the fourth problem of homework 5.
  • Apr 14. Jeff's office hours on Apr 15 are cancelled. Send email if you need to meet.
  • Apr 8. Here is a sample solution to the first three problems of homework 5.
  • Apr 7. Project 3 is available.
  • Apr 7. Here is a sample solution to the aeval_big_small lemma, thanks to Hassan and Hosasm.
  • Apr 1. Correction: h5 is due *April 8*. Here is the latex source for homework 5, in case it's helpful in writing up your solutions. (You do not need to write your answers in tex; hand-written solutions are fine.)
  • Apr 1. Some typos in the operational semantics (Figure 1) in Homework 5 have been fixed.
  • Mar 30. Homework 5 is available. Remember to contact me about your class project by April 10. Homework 4 is also now due Tuesday, March 31, at 23:59:59.
  • Mar 25. Semantics.v has been updated as stated in class.
  • Mar 11. The fourth Coq homework assignment is ready (Semantics.v).
  • Mar 9. Here's a solution to the reverse helper problem: Rev-soln.v.
  • Mar 9. The third Coq homework assignment is ready (Ind.v, Logic.v).
  • Mar 2. The second Coq homework assignment is now ready. Get the latest copy of Poly.v and complete the exercises marked CMSC 631.
  • Feb 22. The first Coq homework assignment is now ready. Get the latest copy of Basics.v and Lists.v from the web page, and complete the exercises marked CMSC 631.
  • Feb 11. Project 2 is now available.
  • Feb 9. Two readings on dataflow analysis have been posted on the schedule web page. Please read the second one, on SSA, by class on Wednesday.
  • Feb 2. Project 1 is now available.
  • Jan 26. Lecture material from today is posted on the schedule web page. (In the future, I'll post material there silently.)

Location CSIC 2120, MW 3:30-4:45pm
Final Exam Take home, available May 10-13
Final Project Due May 20, 2009, by email
Instructor Jeff Foster
4129 A.V. Williams
Hours: MW 1:30-2:30, or by appointment
Textbook None (but see recommendations)
Course evalations are available April 28-May 13. If you're TAing this semester, please encourage your students to also complete evaluations.


This core course is about techniques for analyzing and understanding software artifacts. Ultimately, the goal of this area of study is to improve the quality of software. We will cover three related areas of programming languages research:

  1. Static analysis, the name for any automatic technique for reasoning about program source code. We will study data flow analysis and type systems, and more briefly theorem proving. Model checking will be covered by CMSC 630, offered in Spring 2007.
  2. Formal systems for describing languages and programs, including lambda calculus and axiomatic, denotational, and operational semantics.
  3. Programming language features and how they affect software, including imperative, functional, and object-oriented programming.

Prerequisite: CMSC 430 or equivalent. Most of the material covered in a typical compilers course (CMSC 430) will not be used in this class, so even if you have not taken such a course you may be fine in 631. Contact the instructor if you are interested in taking 631 but aren't sure if you have the background.

Grading and Expectations

Subject to change, especially until the start of the semester.

The final course grade will be made up of the following components:

  • Homework and Programming Assignments (30%) During the semester, there will be several short written homework assignments; a few programming assignments; and assignments using the Coq proof assistant.
  • Project (35%) You will be expected to complete a substantial research project during the semester. Projects may be completed individually or in pairs. For more details, see the projects page.
  • Participation and Presentation (10%) You will present your project to the class, and if there is time, we will include student presentations of existing papers (probably on static analysis tools). Here are the criteria for grading presentations. You will also be graded on contributions to class discussion.
  • Final Exam (25%) This course will include a final exam, which will cover material from the homeworks, programming assginments, and other lecture material.

Late Policy

Written assignments are due at the beginning of class on the due date. Programming assignments (or assignments developed in Coq) are due at midnight on the due date. Neither written nor programming assignments may be turned in late. If you cannot make a due date because of extenuating circumstances, or because it conflicts with a religious holiday, please inform the instructor as soon as possible.

Academic Dishonesty

The college policy on academic dishonesty is strictly followed. All graded materials must be strictly individual efforts. Projects may include collaboration as permitted by the instructor.

Valid HTML 4.01!