Formal Semantics of Programming Languages

Seminar in Theoretical CS, Winter Semester 2019/20

News

  • 01.07.2019: We are online.

Dates & Deadlines

9 Oct, 15:30Kick-off meeting at seminar room of i2 (building E1, room 4201b)
14 OctTopic preferences due
4 NovDetailed outline due
2 DecFull report due
13 JanPresentation slides due
28 JanSeminar 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:30Samir Majeri, Jona Stubbe, Markus Miliats
10:45-11:15Janko Matthes
Afternoon session
14:00-15:30Alexander Immel, Marc Luqué, Daniel Basgöze
15:45-17:15Florian 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)
  2. Hoare logics for recursive procedures and unbounded nondeterminism (B/M)
  3. Semantics of probabilistic programs (B/M)

Concurrency

  1. Formal justification of a proof system for Communicating Sequential Processes (B/M)
    • Supervisor: –
    • Student: –
  2. A Compositional Proof System for Shared Variable Concurrency (B/M)
  3. Generative Operational Semantics for Relaxed Memory Models (M)
  4. Compositional Modeling Formalisms for Hard and Softly Timed Systems (B/M)
  5. Semantics of Petri Nets (B/M)
  6. Model checking for weakly consistent libraries (M)
    • Student: Jona Stubbe

Pointers and Objects

  1. Compositional Shape Analysis (B/M)
  2. Concurrent separation logic I (M)
  3. Concurrent separation logic II (M)
  4. Featherweight Java (B/M)

Software Verification

  1. Property Checking Array Programs Using Loop Shrinking (M)
  2. Software Verification with Property-Directed Reachability (B/M)
    • 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)

Reliability, Privacy and Security

  1. Semantics of dynamic fault trees (B/M)
  2. State/event fault trees (B/M)
    • Student: –
  3. Programming language techniques for differential privacy (B/M)
  4. Verification of information-flow security (B/M)

Additional Material

Registration

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

Contact

Thomas Noll