Seminar in Theoretical CS, Summer 2025

News

• 04.12.2024: we are online

Dates & Deadlines

Early April 2025	Kick-off meeting (room 4201b, 2nd floor, building E1, CS Department)
TBA	Topic preferences due
TBA	Detailed outline due
TBA	Seminar report due
TBA	Presentation slides due
Mid-July 2025	Presentations (room 4201b, 2nd floor, building E1, CS Department)

Note that the full versions of your report and your slides should be your final submissionand 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.

Introduction

• Slides of introduction
• Topic choice form

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 logical approaches over deductive program verification to the analysis of quantum programs.

Topics (preliminary)

The following list gives an exemplary of topics to choose from. More entries will be added soon.

A. Hoare Logic

1. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism
   • Literature: T. Nipkow: Hoare logics for recursive procedures and unbounded nondeterminism, CSL 2002
   • Student: –
   • Supervisor: –
2. Incorrectness Logic
   • Literature: Peter W. O’Hearn: Incorrectness Logic, POPL 2020
   • Student: –
   • Supervisor: –
3. Outcome Logic
   • Literature: Noam Zilberstein, Derek Dreyer, Alexandra Silva: Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning, OOPSLA 2023
   • Student: –
   • Supervisor: –
4. A Taxonomy of Hoare-Like Logics
   • Literature: Lena Verscht, Benjamin Lucien Kaminski: A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests, POPL 2025
   • Student: –
   • Supervisor: –

B. Separation Logic

1. Introduction to Separation Logic
   • Literature: Peter W. O’Hearn: A Primer on Separation Logic (and Automatic Program Verification and Analysis), Software Safety and Security, 2012
   • Student: –
   • Supervisor: –
2. Formalising Memory Safety
   • Literature: Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce: The Meaning of Memory Safety, POST 2018
   • Student: –
   • Supervisor: –
3. Semantics of Concurrent Pointer Programs
   • Literature: Viktor Vafeiadis: Concurrent Separation Logic and Operational Semantics. ENTCS 276 (2011)
   • Student: –
   • Supervisor: –

C. Software Verification

1. Reasoning About Termination
   • Literature: Rupak Majumdar, V. R. Sathiyanarayana: Sound and Complete Techniques for Reasoning About Termination, Springer LNS 15260, 2025
   • Student: –
   • Supervisor: –
2. Verification by Transformation
   • Literature: Dirk Beyer, Nian-Ze Lee: The Transformation Game: Joining Forces for Verification, Springer LNS 15262, 2025
   • Student: –
   • Supervisor: –

D. Static Analysis of Quantum Programs

1. Detecting Bugs
   • Literature: Pengzhan Zhao, Xiongfei Wu, Zhuo Li, Jianjun Zhao: QChecker: Detecting Bugs in Quantum Programs via Static Analysis, Q-SE 2023
   • Student: –
   • Supervisor: Thomas Noll
2. Entanglement Analysis
   • Literature: Shangzhou Xia, Jianjun Zhao: Static Entanglement Analysis of Quantum Programs, Q-SE 2023
   • Student: –
   • Supervisor: Thomas Noll
3. The LintQ Static Analysis Framework
   • Literature: Matteo Paltenghi, Michael Pradel: Analyzing Quantum Programs with LintQ: A Static Analysis Framework for Qiskit, FSE 2024
   • Student: –
   • Supervisor: Thomas Noll

Prerequisites

Basic knowledge in the following areas is expected:

• Formal languages and automata theory
• Mathematical logic

Previous knowledge in formal semantics of programming languages and probabilistic or quantum programming (depending on the choice of the topic) is helpful but not mandatory.

Registration

Registration to the seminar is handled via the central SuPra system.

Grading Scheme

You can access the grading scheme here.

• Report template
• Presentation template
• How to Write a Seminar Paper
• Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
• How to Give Presentations
• Introduction to LaTeX

Contact

Thomas Noll