Verfication of Concurrent, Distributed Software

The seminar focuses on the study of modern lightweight verification techniques such as type systems for concurrent, distributed programs. It will cover type systems for general distributed systems and specific ones such cryptographic protocols, stream processing, multicore computing, multi-organisational applications and parallel computations.

There are no frontal lessons: you will have to write a term paper that summarizes your knowledge of an assigned topic after reading a selection of scientific papers. Each participant is also required to give a talk about the topic chosen. Several topics are available, proposals from students can also be evaluated.

Course Information



Course Type

S2 / 3 CPs


Andi Bejleri


Please send an email to the instructor


14th October, 14:25-16:05 in S202/A126




Both papers and talks must be delivered in English


With this seminar we want to introduce you to core techniques of scientific work; each participant is thus required to give a talk about the topic chosen. This talk will be given during a Blockseminar at the end of the term.

All talks have to be 20 minutes long if given by a single person, and 30 minutes or 35 minutes when given by a group of two or three, respectively. (Each member of the group should have an equal share in it.) Please practice your talk several times; in particular, make sure that you do not miss the time limit by much, i.e., by at most 10%; this mimics the strict time limits of real-world conferences and workshops. Consequently, if a talk is significantly shorter or longer, then this fact will have a (negative) impact on the presenters' grade.

Term Paper

In addition to giving scientific talks, we want to introduce you to the process of writing and publishing research papers. In other words: you will have to write a term paper. The following notes may guide you in this process:

The initial references provided with the topic chosen by you are only a first step; in your term paper, try not to summarize everything that's written therein or in the references' references. Instead, try to tell an engaging, coherent story about one aspect of the topic. (It helps to image oneself as a novice to the topic, who attends the talks or reads the term papers.) Also, search for further references on your own and point out connections between the various papers you researched; we expect at least 2-3 related references found per person. Please present technologies, e.g., programming languages, with your own words and your own examples. If you merely copy the work of others, this means but one thing: no contribution; you will fail the seminar. This rule does not prevent you from quoting other researchers, however. It does require you to faithfully attribute quotations or other kinds of references, though.

Overall, we expect about 6 pages of term paper if written by a single person. For groups of two or three persons we expected 8 or 10 pages, respectively. (This page limit take the space needed for the title, the list of references, and any figures already into account.) If many or large figures or tables are included, we expect a slightly longer term paper to compensate for this. Please consult your advisor about this. To make the term papers' length comparable, all participants are required to use the ACM SIGPLAN Proceedings Template, preferably in its LaTeX incarnation (default font size, 9pt).


The overall grade for the seminar is determined by two factors: the talk given and the paper handed in. Furthermore, we will consider your participation in the discussion following each talk; it counts towards the grade received for your reviews. Overall, the three factors are weighted 35 : 65, respectively.

Please note that it is possible, due to the fact that each participants talk and reviews are graded individually, that different members of a group are assigned different overall grades.