Overview
This course covers modern program analysis and synthesis techniques. Due to their automation, scalability, and applicability to a wide range of problems, these techniques have become increasingly popular in the last decade.
Program analysis refers to a set of techniques for automated program reasoning. These techniques have enabled many interesting applications: security and correctness of complex systems (e.g., mobile apps, algorithms, drivers, networks, etc), automating inference in machine learning (e.g., probabilitic programs), analysis of biological systems (e.g., DNA computations), discovering asymptotic complexity of algorithms, and many more.
Program synthesis techniques are emerging as an exciting new way for constructing programs (e.g., from examples, from partial specs, etc), combining advanced search algorithms, statistical learning and constraint solving techniques (e.g., SMT). These new synthesis approaches have been applied to many areas including end-user programming, discovery of algorithms, security policies, and many more.
This course will cover the core principles behind these automated techniques as well as the most interesting recent research developments and practical applications. There will be a hands-on project where students will build program analyzers or synthesizers.