Available courses

Program analysis can be used to find or to show the absence of certain kinds of bad program behaviours, e.g. division by zero, null-pointer access, etc., in general fully automatically.

In this course, we will

  • introduce the theoretical foundation of many static analysis techniques (data flow analysis, abstract interpretation)
  • present the main types of dynamic techniques (fuzz testing, symbolic execution)
  • discuss the tradeoffs in efficiency, accuracy, and soundness between the different techniques
  • show applications of program analysis techniques in various application areas
Logistics

The first class will take place on Tuesday, 23 October.

Prerequisites

While there are no formal pre-requisites for the class, it is intended for advanced Bachelor or Master students. Previous classes on semantics, automated reasoning, verification or compiler construction are helpful, but not necessary.


Program analysis can be used to find or to show the absence of certain kinds of bad program behaviours, e.g. division by zero, null-pointer access, etc., in general fully automatically.

In this course, we will

  • introduce the theoretical foundation of many static analysis techniques (data flow analysis, abstract interpretation)
  • present the main types of dynamic techniques (fuzz testing, symbolic execution)
  • discuss the tradeoffs in efficiency, accuracy, and soundness between the different techniques
  • show applications of program analysis techniques in various application areas
Logistics

The first class will take place on Tuesday, 16 October.

Prerequisites

While there are no formal pre-requisites for the class, it is intended for advanced Bachelor or Master students. The following classes are helpful, but not necessary: Automated Reasoning, Semantics, Verification, Compiler Construction.


This course covers advanced topics of automata theory and its applications (e.g., computer-aided verification), including:

  • learning of automata
  • the connection of automata to second-order logic and Linear Temporal Logic
  • automata on infinite words
  • automata on trees
  • synthesis of reactive systems

Intended Audience: The course is intended for computer science or math students with background in logic and theory of computation (familiarity with basic algorithms, logic, and the theory of computation will be assumed). Talk to the instructor if you are not sure if you have the background. Please attend the initial lecture for background material.

Further, students should (1) have "mathematical maturity" (e.g., you should be comfortable with proofs and abstract reasoning), (2) be interested in the material; and (3) are willing to spend time outside of class in order to better understand the material presented in lectures.


The idea that we could tell a computer what we want and it would automatically figure out how to achieve it has fascinated scientists for a long time, but it has also been an elusive goal. Via recent research papers in the area of program synthesis, this seminar will look at the significant steps which have been made towards this grand vision. We will discuss what is currently possible, for which application domains program synthesis is successful, what the main challenges are and what perhaps will never be feasible. The paper selection will cover the major synthesis techniques to provide an overview of the current landscape.

Course website