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 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.

Schedule of Talks

Morning session
09:00-10:30	Samir Majeri, Jona Stubbe, Markus Miliats
10:45-11:15	Janko Matthes
Afternoon session
14:00-15:30	Alexander Immel, Marc Luqué, Daniel Basgöze
15:45-17:15	Florian Keßler, Mohamed Khalifa, Jord Piciri

Topics

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

Recursion, Nondeterminism and Probabilities

1. 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
2. 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: –
   • Student: –
3. 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

1. 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: –
2. 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
3. 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: –
   • Student: –
4. 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
5. 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
6. 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

1. 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
2. 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: –
3. Concurrent separation logic II (M)
   • Literature: Viktor Vafeiadis: Concurrent Separation Logic and Operational Semantics. ENTCS 276:335-351, 2011.
   • Supervisor: –
   • Student: –
4. 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

1. 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é
2. 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: –
3. 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: –
   • Student: –
4. 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

1. 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
2. State/event fault trees (B/M)
   • Literature: Bernhard Kaiser, Catharina Gramlich, Marc Förster: State/event fault trees—A safety analysis model for software-controlled systems. RESS 2017
   • Supervisor: –
   • Student: –
3. 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: –
   • Student: –
4. 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.

Contact

Thomas Noll