Available courses

Program analysis refers to a collection of techniques that infers global or local properties of programs. It has applications in several areas: in compiler optimizations, program testing, numerical programming, probabilistic programing, security, and various other domains. This block seminar will survey different applications of both static and dynamic program analysis based on recent research papers. The goal of the seminar is to give an overview of these advanced analyses and how the application areas benefit from the techniques used.

We would like to start a series of 'townhall talks' at the institute, which will feature a mix of technical overview, as well as communication, presentation, and other research skills talks. The technical overview talks will be high-level presentations about a group's current research. The research skills talks are meant to complement Rose's communication classes and support, and will be usually followed by a (panel) discussion, i.e. they are meant to be interactive. Everyone is encouraged to participate!

The talks are scheduled roughly every 6 weeks.


This course will cover both the writing process and the writing product. You will learn writing principles that will you help you to create text that is coherent, cohesive, and clear. A primary goal of this course is to teach you how to "escape" your own expertise in order to identify the parts of your text that will cause a reader difficulties. 

The course format will vary from week-to-week, and will include a mix of mini-lectures, exercises, one-on-one feedback, and group discussions of part of a paper (usually written by a course participant but sometimes selected from the literature). In order to get the most out of the class, participants will be expected to do substantial out-of-class writing (about one to two hours per week). The precise content of the course will be tailored to the course participants.

Prerequisites

This course is intended for PhD students and postdocs in Computer Science. For PhD students, I typically prefer that students have already taken my course on how to give scientific presentations. I do make exceptions, but students need to demonstrate that they already have basic competence at communicating scientific ideas verbally.


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

Advanced course at Universität des Saarlandes

6 credit points
Summer semester 2019

This course introduces two topics together

  • The first part is a self-contained introduction to the proof assistant Isabelle/HOL.
  • The second part is an introduction to the semantics of imperative programming languages. This part is formalized in Isabelle.

This advanced course is based on a book by Prof. Tobias Nipkow and Prof. Gerwin Klein, which is available both as a free PDF online and as a hardcover from Springer. The material is complementary to the core Semantics course by Prof. Gert Smolka, which uses Coq and focuses on the λ-calculus and functional programming.

Proof assistants are tools that allow its users to carry out mathematical proofs rigorously, based on a logical foundation. Developing a proof in a proof asssistant as opposed to using pen and paper is roughly the equivalent of programming on a computer as opposed to sketching pseudocode on paper. Expertise with proof assistants is becoming an increasingly important skill, especially for software verification, which aims at proving the absence of bugs in programs. In the experience of many instructors, the use of a proof assistant helps students get a good grip on computer science topics.

Coq and Isabelle are the main two proof assistants in use. Isabelle's strength is that it is simple as 1-2-3: It offers (1) a simple yet powerful logic, (2) a convenient user interface, and (3) a lot of proof automation.

There are no formal prerequisites for taking the course. Familiarity with a typed functional programming language (such as Standard ML, OCaml, Haskell, or F#), as taught in Programmierung 1, is highly recommended.