Fundamentals of Program Analysis
This MIT OpenCourseWare course introduces the theory and practice of program analysis, the techniques compilers and verification tools use to reason about what a program will do before it runs. Lectures cover type checking and its underlying type systems, abstract interpretation for approximating program behavior, and model checking for verifying properties against a state space. Each topic pairs formal foundations, such as soundness and lattice theory, with modern applications in software verification and bug detection. Materials include lecture notes, readings, and problem sets drawn from MIT's graduate-level treatment of the subject. The course assumes some background in programming languages or compilers and works through the mathematical machinery behind each analysis technique rather than just tool usage. No certificate is offered, consistent with MIT OCW's open publication of course materials.