Seminar in Theoretical CS, Winter 2021/22

News

• 01.06.2021: we are online

Dates & Deadlines

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

Introduction and Assignment of Topics

• Slides of introduction
• Foodle poll for topic assignment

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

Time	Thursday, February 3
09:00-10:30	Gergana Tropcheva, Jonathan Müller, Sebastian Bartsch
11:00-12:00	Niklas Klosterhalfen, Jannik Eickelmann
13:00-14:00	Anike Heikrodt, Frithjof Petrick
14:30-15:30	Katherine 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)
   • Paper: Peter W. O’Hearn: A Primer on Separation Logic (and Automatic Program Verification and Analysis). Software Safety and Security – Tools for Analysis and Verification. NATO Science for Peace and Security Series, vol 33, 286-318, 2012
   • Student: Gergana Tropcheva
   • Supervisor: Ira Fesefeldt
2. Formalising Memory Safety (B)
   • Paper: Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce: The Meaning of Memory Safety. POST 2018: 79-105
   • Student: Niklas Klosterhalfen
   • Supervisor: Thomas Noll
3. Reasoning about Incorrectness (B)
   • Paper: Peter W. O’Hearn: Incorrectness Logic. POPL 2020, Article 10
   • Student: Jannik Eickelmann
   • Supervisor: Thomas Noll
4. Logics for Object-Oriented Programs (B)
   • Paper: Cees Pierik, Frank S. de Boer: A proof outline logic for object-oriented programming. TCS 343(3), 2005
   • Student: –
   • Supervisor: –
5. Semantics of Concurrent Pointer Programs (M)
   • Paper: Viktor Vafeiadis: Concurrent Separation Logic and Operational Semantics. ENTCS 276 (2011), 335-351
   • Student: Jonathan Müller
   • Supervisor: Ira Fesefeldt
6. A Meta-Framework: Views (M)
   • Paper: Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, Hongseok Yang: Views: compositional reasoning for concurrent programs. POPL 2013, 287-300
   • Student: Sebastian Bartsch
   • Supervisor: Ira Fesefeldt

Program Synthesis

7. 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: –
8. Synthesis as Verification (B)
   • Paper: Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster: From program verification to program synthesis. POPL 2010, 313-326
   • Student: –
   • Supervisor: –
9. 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
10. Program Sketching (B)
    • Paper: Armando Solar-Lezama: Program sketching. STTT 15, 475–495 (2013)
    • Student: –
    • Supervisor: –
11. Component-Based Synthesis (B)
    • Paper: Kensen Shi, Jacob Steinhardt, Percy Liang: FrAngel: component-based synthesis with control structures. POPL 2019
    • Student: –
    • Supervisor: –
12. Synthesising Pointer Programs (M)
    • Paper: Nadia Polikarpova, Ilya Sergey: Structuring the Synthesis of Heap-Manipulating Programs. POPL 2019
    • Student: Frithjof Petrick
    • Supervisor: Jip Spel
13. Synthesising Probabilistic Programs (M)
    • Paper: A.V. Nori, S. Ozair, S.K. Rajamani, D. Vijaykeerthy: Efficient synthesis of probabilistic programs. PLDI 2015
    • Student: –
    • Supervisor: –

Analysing Probabilistic Systems

14. Slicing Probabilistic Programs (B)
    • Paper: C.K. Hur, A.V. Nori, S.K. Rajamani, S. Samuel: Slicing Probabilistic Programs. PLDI 2014
    • Student: –
    • Supervisor: –
15. Probabilistic Termination (M)
    • Paper: Luis Maria Ferrer Fioriti, Holger Hermanns: Probabilistic Termination: Soundness, Completeness, and Compositionality. POPL 2015
    • Student: Katherine Cornell
    • Supervisor: Lutz Klinkenberg
16. Moment Analysis (M)
    • Paper: Di Wang, Jan Hoffmann, Thomas Reps: Central Moment Analysis for Cost Accumulators in Probabilistic Programs. PLDI 2021
    • Student: –
    • Supervisor: –
17. Runtime Monitoring of Probabilistic Systems (M)
    • Paper: Sebastian Junges, Hazem Torfah, Sanjit A. Seshia: Runtime Monitoring for Markov Decision Processes. arXiv:2105.12322 (2021)
    • Student: –
    • Supervisor: –
18. Model Checking of Probabilistic Systems (M)
    • Paper: Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, Guy Van den Broeck: Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. arXiv:2105.12326 (2021)
    • Student: –
    • Supervisor: –

Robotic Applications

19. A Modelling Language for Robotic Systems (B)
    • Paper: Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, Jim Woodcock: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5): 3097-3149 (2019)
    • Student: Parsa Bahadori
    • Supervisor: Shahid Khan
20. Generation of Mobile Robot Controllers (M)
    • Paper: Bruno Lacerda, David Parker, Nick Hawes: Multi-Objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. Automated Planning and Scheduling, 27(1), 504-512
    • Student: –
    • Supervisor: –

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

• Report template
• Presentation template
• How to Write a Seminar Paper
• Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
• How to Give Presentations
  • How to Design Talks (video, starting at 1:01:12)
  • How to Give a Great Research Talk (video)
• Introduction to LaTeX

Contact

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