Fundamentals of program analysis

Lectures: 2 sessions / week, 1.5 hours / session

Optional Recitations: 1 session / week, 1 hour / session

6.035 Computer Language Engineering

This course offers a comprehensive introduction to the field of program analysis. It covers some of the major forms of program analysis including Type Checking, Abstract Interpretation and Model Checking. For each of these, the course covers the underlying theories as well as modern techniques and applications.

Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. ISBN: 9780262162098. [Preview with Google Books]

Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. ISBN: 9780262731034. [Preview with Google Books]

Nielson, Nielson, and Hankin. Principles of Program Analysis. Springer, 2010. ISBN: 9783642084744.

Baier, and Katoen. Principles of Model Checking. MIT Press, 2008. ISBN: 9780262026499.

This course used the Coq Proof Assistant Software for some assignments. Students aren't expected to become experts on Coq, but here are some Coq resources anyway:

Chlipala, Adam. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. ISBN: 9780262026659. [Preview with Google Books] (not yet available in print, but a draft is available Online)

Pierce, Benjamin C., et al. Software Foundations.

Bertot, Yves, and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. ISBN: 9783540208549. [Preview with Google Books]

Course topics include 6 units.

Unit 1: Intro to Functional Programming & Operational Semantics

Unit 2: Type Theory

Unit 3: Types for Imperative Programs

Unit 4: Axiomatic Semantics

Unit 5: Abstract Interpretation

Unit 6: Model Checking

There are 6 homework assignments. They consist of problem sets and programming assignments relating to the material covered in class. Homework is due no later than 5:00 pm on the day marked in the assignment handout; late homework is accepted with a 10% penalty for each day of delay (maximum 3 days; talk to the instructor if there are special circumstances that may require more).

Don't show me this again

This is one of over 2,200 courses on OCW. Find materials for this course in the pages linked along the left.

MIT OpenCourseWare is a free & open publication of material from thousands of MIT courses, covering the entire MIT curriculum.

No enrollment or registration. Freely browse and use OCW materials at your own pace. There's no signup, and no start or end dates.

Knowledge is your reward. Use OCW to guide your own life-long learning, or to teach others. We don't offer credit or certification for using OCW.

Made for sharing. Download files for later. Send to friends and colleagues. Modify, remix, and reuse (just remember to cite OCW as the source.)

Learn more at Get Started with MIT OpenCourseWare