Advanced Topics in Formal Semantics (Seminar)

Seminar in Theoretical CS, Winter 2021/22

News

  • 01.06.2021: we are online

Dates & Deadlines

13.10.2021, 14:00Introduction
20.10.2021Topic preferences due
15.11.2021Detailed outline due
13.12.2021Seminar report due
17.01.2022Presentation slides due
03.02.2022Seminar talks

Introduction and Assignment of Topics

Overview

The term semantics refers to the rigorous mathematical study of the meaning and behaviour of software systems. Several methods have been established to provide this meaning, depending on both the kind of system to be modelled and the purpose of the analysis. Having a clear and comprehensive understanding of what it means to execute a program supports the development, implementation, analysis and verification of software systems.

The goal of this seminar is to provide an overview of semantics-based techniques and their applications in various fields, ranging from program verification and synthesis over probabilistic systems to robotic application.

Schedule of Talks

TimeThursday, February 3
09:00-10:30Gergana Tropcheva, Jonathan Müller, Sebastian Bartsch
11:00-12:00Niklas Klosterhalfen, Jan Eickelmann
13:00-14:00Anike Heikrodt, Frithjof Petrick
14:30-15:30Katherine Cornell, Parsa Bahadori

Topics

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

Analysing Heap-Manipulating Programs

  1. Introduction to Separation Logic (B)
  2. Formalising Memory Safety (B)
  3. Reasoning about Incorrectness (B)
  4. Logics for Object-Oriented Programs (B)
  5. Semantics of Concurrent Pointer Programs (M)
  6. A Meta-Framework: Views (M)

Program Synthesis

  1. Applications of Program Synthesis (B)
    • Paper: Sumit Gulwani, Oleksandr Polozov, Rishabh Singh: Program Synthesis. Chapter 2: Applications. Programming Languages 4(1-2), 2017
    • Student: –
    • Supervisor: –
  2. Synthesis as Verification (B)
  3. Syntax-Guided Synthesis (B)
    • Paper: R. Alur, R. Bodik, G. Juniwal, M.M.K. Martin, M. Raghothaman, S.A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, A. Udupa: Syntax-guided synthesis. FMCAD 2013
    • Student: Anike Heikrodt
    • Supervisor: Jip Spel
  4. Program Sketching (B)
    • Paper: Armando Solar-Lezama: Program sketching. STTT 15, 475–495 (2013)
    • Student: –
    • Supervisor: –
  5. Component-Based Synthesis (B)
  6. Synthesising Pointer Programs (M)
  7. Synthesising Probabilistic Programs (M)

Analysing Probabilistic Systems

  1. Slicing Probabilistic Programs (B)
  2. Probabilistic Termination (M)
  3. Moment Analysis (M)
  4. Runtime Monitoring of Probabilistic Systems (M)
  5. Model Checking of Probabilistic Systems (M)

Robotic Applications

  1. A Modelling Language for Robotic Systems (B)
  2. Generation of Mobile Robot Controllers (M)

Prerequisites

Depending on the chosen topic, basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Probability Theory

Previous knowledge in semantics of programming languages, probabilistic programming and model checking is helpful but not mandatory

Registration

Registration to the seminar is handled via SuPra. Later registrations are not possible.

Additional Material

Contact

Thomas Noll <noll at cs.rwth-aachen.de>