
 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; handwritten 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: Revsoln.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:304:45pm


Final Exam
 Take home, available May 1013


Final Project
 Due May 20, 2009, by email


Instructor
 Jeff Foster
4129 A.V. Williams
Hours: MW 1:302:30, or by appointment


Textbook
 None (but see recommendations)


Course evalations are available
April 28May 13. If you're TAing this semester, please encourage
your students to also complete evaluations.
Description
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:
 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.
 Formal systems for describing languages and
programs, including lambda calculus and axiomatic, denotational, and
operational semantics.
 Programming language features and
how they affect software, including imperative, functional, and
objectoriented 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.
