MIT OpenCourseWare
Fundamentals of Program Analysis
Art: not stated, Fletcher's Combined Block Telegraph Apparatus and Bell, 1889 · Public domain
- Instructor
- Prof. Armando Solar-Lezama
- Term
- Fall 2015
- Level
- Undergraduate
- What's inside
- 1 problem set · 1 lecture note · 1 reading · 37 other files · 2 web pages
- Materials open
- MIT OCW
About this course
Source: MIT OpenCourseWare 6.820 Fundamentals of Program Analysis, Fall 2015, Prof. Armando Solar-Lezama — original course page on ocw.mit.edu ↗. License: CC BY-NC-SA 4.0. Study order: none is claimed; materials are grouped by MIT's own sections. Taken from MIT's published course files, downloaded from ocw.mit.edu on September 23, 2026. How RedLectern is built.
Materials are grouped the way MIT organized them. A verified, course-wide order has not been established here.
Before you start
Prerequisites are not listed here. Check MIT's own syllabus for this course.
How this course was organized
What's here, and what isn't
- MIT lists a session calendar for this course, but it could not be verified well enough to build a sequence from it — materials are grouped by section instead.
Not included here
24 items from the source could not be safely included:
- MIT's page format for this item wasn't recognized clearly enough to place it safely. (23 items)
- Referenced in a table, but without MIT's own verified order, so it isn't used to claim a sequence.
Materials by section
Grouped by section, as MIT organized them. Not sequenced or ordered.
Lecture Notes
27 files
- Abstract Interpretation, Galois Connections (cont.), Lecture 19 Download
- Algebraic Data Types & Their Ingredients: Product, Sum, and Recursive Types, Lecture 7 Download
- Axiomatic Semantics for Concurrency: Rely-Guarantee & Concurrent Separation Logic, Lecture 16 Download
- Big-Step vs. Small-Step Semantics and the λLet Calculus, Lecture 3 Download
- Coq Crash Course (Examples in Operational Semantics), Lecture 4 Download
- Coq Examples, Lecture 5 Download
- Dataflow Analysis and Abstract Interpretation, Lecture 18 Download
- Dataflow Analysis, Lattices, Fixed Points, Lecture 17 Download
- Explicit State Model Checking, Lecture 23 Download
- From Model Checking to Synthesis, Lecture 26 Download
- Hindley-Milner Type Inference and Polymorphic Types, Lecture 6 Download
- Intro to Axiomatic Semantics, Lecture 12 Download
- Intro to Models and Properties, Lectures 21 Download
- Introduction to Functional Programming and Types, Lecture 1 Download
- Introduction to Simple Types, Lecture 5 Download
- Lambda Calculus, Lecture 2 Download
- Monads, Lecture 9 Download
- Separation Logic, Lecture 15 Download
- Software Model Checking with Abstraction Refinement, Lecture 25 Download
- Symbolic Model Checking, Lecture 24 Download
- Temporal Logic, Lecture 22 Download
- The Heap: Inferring Loop Invariants about Data Structure Shape, Lecture 20 Download
- Total Correctness and Termination, Lecture 14 Download
- Type Classes and Subtyping, Lecture 8 Download
- Typing of Imperative Programs, Lecture 10 Download
- Verification Condition Generation, Lecture 13 Download
- Verification of Complex Properties with Types: From Information Flow to Race Detection, Lecture 11 Download
Assignments
11 files
- Fundamentals of Program Analysis Assignment 1 Download
- Fundamentals of Program Analysis Assignment 2 Download
- Fundamentals of Program Analysis Assignment 3 Download
- Fundamentals of Program Analysis Assignment 4 Download
- Fundamentals of Program Analysis Assignment 5 Download
- Fundamentals of Program Analysis Assignment 6 Download
- ps2Code Download
- ps2CoqCode Download
- ps3Code Download
- ps4Code Download
- pset5 Download
MIT OpenCourseWare, Prof. Armando Solar-Lezama, 6.820 Fundamentals of Program Analysis, Fall 2015.
License: CC BY-NC-SA 4.0 · Edition: Fall 2015 · Open the original course on OCW ↗
Organized by RedLectern, independent of MIT and not endorsed by MIT.
Per-resource rights are recorded on each resource; All-Rights-Reserved items are link-only, never mirrored.