2400188 – Type Systems and Static Program Analysis

Static type systems and program analyses predict the behavior of programs through source-code analysis, but without executing the program. They are fundamental for isolating ill-defined program behavior (e.g., from type errors), but can also find bugs or also can provide guarantees (e.g., memory safety). The first part of this course, which is designed as a self-study, is concerned about type systems, their definition, formalization, properties and features such as inheritance and polymorphism. The second half, delivered through on-site lectures, covers a broader class of static program analyses, including data-flow analysis, points-to analysis, and control-flow analysis, and provides an introduction to abstract interpretation.