Seminar in Theoretical CS, Winter Semester 2019/20

## News

- 01.07.2019: We are online.

## Dates & Deadlines

9 Oct, 15:30 | Kick-off meeting at seminar room of i2 (building E1, room 4201b) |

14 Oct | Topic preferences due |

4 Nov | Detailed outline due |

2 Dec | Full report due |

13 Jan | Presentation slides due |

28/29 Jan (?) | Seminar talks |

Note that the non-camera-ready versions of your report and your slides should be your *final submission* and the camera-ready versions should differ only with regard to *minor* remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting *preliminary versions before the due dates*.

## Overview

In programming language theory, the term *semantics* refers to the rigorous mathematical study of the meaning of programs. Several methods have been established to provide this meaning for various kinds of programming languages. Having a clear and comprehensive understanding of what it means to execute a program supports the development of both new programming languages, their compilers, and individual programs. Moreover, it constitutes the basis for the analysis and verification of software systems.

The aim of this seminar is twofold. On the one side, it provides introductory topics on bachelor level (“*Introduction to Formal Semantics of Programming Languages*“). On the other side, it extends the contents of the course on *Semantics and Verification of Software* from the previous summer term (“*Advanced Topics in Formal Semantics of Programming Languages*“).

## Prerequisites

Basic knowledge in the following areas is expected:

- Programming
- Automata theory
- Mathematical logic
- For advanced topics, previous knowledge in formal semantics of programming languages is very helpful.

## Topics

(The annotations “B” and “M” respectively refer to topics on Bachelor and Master level.)

### Recursion, Nondeterminism and Probabilities

- Proving total correctness of recursive procedures (B/M)
**Literature:**P. America and F. S. de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2):129–162, 1990.**Supervisor:**Jip Spel**Student:**Luisa Lux

- Hoare logics for recursive procedures and unbounded nondeterminism (B/M)
**Literature:**T. Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. CSL 2002, volume 2471 of Lecture Notes in Computer Science, pages 103–119. Springer, 2002.**Supervisor:**Jip Spel**Student:**Yeyung Yoon

- Semantics of probabilistic programs (B/M)
**Literature:**Aditya Nori, Chung-Kil Hur, Sriram Rajamani, Selva Samuel: R2: An Efficient MCMC Sampler for Probabilistic Programs. AAAI 2014**Supervisor:**Marcin Szymczak**Student:**Samir Majeri

### Concurrency

- Formal justification of a proof system for Communicating Sequential Processes (B/M)
**Literature:**- K. R. Apt, N. Francez, W.P. de Roever: A Proof System for Communicating Sequential Processes. ACM TOPLAS 2(3), 1980.
- K. R. Apt: Formal justification of a proof system for Communicating Sequential Processes. Journal of the ACM, 30:197–216, 1983.

**Supervisor:**–**Student:**–

- A Compositional Proof System for Shared Variable Concurrency (B/M)
**Literature:**Frank S. de Boer, Ulrich Hannemann, Willem P. de Roever: A Compositional Proof System for Shared Variable Concurrency. FME 1997: 515-532**Supervisor:**Philipp Berger**Student:**Alexander Immel

- Generative Operational Semantics for Relaxed Memory Models (M)
**Literature:**Radha Jagadeesan, Corin Pitcher, James Riely: Generative Operational Semantics for Relaxed Memory Models. ESOP 2010: 307-326**Supervisor:**Jip Spel**Student:**Andrew Cornell

- Compositional Modeling Formalisms for Hard and Softly Timed Systems (B/M)
**Literature:**Henrik C. Bohnenkamp, Pedro R. D’Argenio, Holger Hermanns, Joost-Pieter Katoen: MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE TSE 32(10): 812-830 (2010)**Supervisor:**Tim Quatmann**Student:**Felix Sebastian Meyer

- Semantics of Petri Nets (B/M)
**Literature:**Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang: A Semantics for Every GSPN. Petri Nets 2013: 90-109**Supervisor:**Tim Quatmann**Student:**Janko Matthes

- Model checking for weakly consistent libraries (M)
**Literature:**Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis: Model checking for weakly consistent libraries. PLDI 2019**Supervisor:**Matthias Volk

**Student:**Jona Stubbe

### Pointers and Objects

- Compositional Shape Analysis (B/M)
**Literature:**- Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, Hongseok Yang: Compositional Shape Analysis by means of Bi-Abduction. POPL 2009
- Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, Hongseok Yang: Compositional Shape Analysis by means of Bi-Abduction. JACM 58(6), 2011

**Supervisor:**Thomas Noll**Student:**Florian Keßler

- Concurrent separation logic I (M)
**Literature:**S. Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375(1-3):227– 270, 2007.**Supervisor:**–**Student:**–

- Concurrent separation logic II (M)
**Literature:**Viktor Vafeiadis: Concurrent Separation Logic and Operational Semantics. ENTCS 276:335-351, 2011.**Supervisor:**–**Student:**–

- Featherweight Java (B/M)
**Literature:**Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3): 396-450 (2001)**Supervisor:**Thomas Noll**Student:**Mohamed Khalifa

### Software Verification

- Property Checking Array Programs Using Loop Shrinking (M)
**Literature:**Shrawan Kumar, Amitabha Sanyal, R. Venkatesh, Punit Shah: Property Checking Array Programs Using Loop Shrinking. TACAS 2018, 213-231**Supervisor:**Philipp Berger**Student:**Marc Luqué

- Software Verification with Property-Directed Reachability (B/M)
**Literature:**Dirk Beyer, Matthias Dangl: Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art, arXiv 1908.06271 (2019)

**Supervisor:**–**Student:**–

- Parser-Directed Fuzzing (B/M)
**Literature:**Björn Mathis, Rahul Gopinath, Michaël Mera, Alexander Kampmann, Matthias Höschele, Andreas Zeller: Parser-Directed Fuzzing. PLDI 2019**Supervisor:**Matthias Volk**Student:**Ji Min Kim

- Analyzing undefined behavior of C programs (B/M)
**Literature:**Chris Hathhorn, Chucky Ellison, Grigore Roşu: Defining the undefinedness of C. PLDI 2015**Supervisor:**Philipp Berger**Student:**Daniel Basgöze

### Reliability, Privacy and Security

- Semantics of dynamic fault trees (B/M)
**Literature:**Antoine Rauzy, Chaire Blériot-Fabre: Towards a sound semantics for dynamic fault trees. RESS 2015**Supervisor:**Matthias Volk**Student:**Markus Miliats

- State/event fault trees (B/M)
**Literature:**Bernhard Kaiser, Catharina Gramlich, MarcFörster: State/event fault trees—A safety analysis model for software-controlled systems. RESS 2017**Supervisor:**–

**Student:**–

- Programming language techniques for differential privacy (B/M)
**Literature:**Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce: Programming language techniques for differential privacy. SIGLOG News 3(1): 34-53 (2016)**Supervisor:**Marcin Szymczak**Student:**Runzhou Li

- Verification of information-flow security (B/M)
**Literature:**David Costanzo, Zhong Shao, Ronghui Gu: End-to-end verification of information-flow security for C and assembly programs. PLDI 2016

**Supervisor:**Thomas Noll**Student:**Jord Piciri

## Additional Material

- Introductory slides
- Report template
- Presentation template
- How to write scientific papers
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to give presentations
- Introduction to LaTeX

## Registration

Registration to the seminar is possible via the central registration procedure of the CS Department.