Seminar in Theoretical CS, Winter 2024/25

News

• 06.06.2024: we are online

Dates & Deadlines

TBA	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
Jan 20-23, 2025	Presentations (room 4201b, 2nd floor, building E1, CS Department)
TBA	Final revision of report

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

Overview

The term Computer-Aided Verification refers to theory and practice of computer-supported formal analysis methods for both hardware and software systems. Likewise, it is the name of an annual academic conference on that topic. The modeling and verification of such systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality.   Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software. Due to the complexity of these approaches and the systems they are applied to, automated computer support is indispensable.  

The goal of this seminar is to give an overview of the related research activities of the MOVES group. It covers several areas of computer science to which computed-aided verification techniques are central, and which represent the research fields of the respective supervisors. Each area features a number of topics which are described in a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation. The following list gives an overview of the areas that will be covered.

Topics (preliminary)

A. Verification of Neural Networks

1. Verification using the Simplex Algorithm
   • Aws Albarghouthi: Introduction to Neural Network Verification, pages 67 – 81
   • Student: –
   • Supervisor: Christopher Brix
2. Abstraction-Based Verification with Intervals and Zonotopes
   • Aws Albarghouthi: Introduction to Neural Network Verification, pages 83 – 108
   • Student: –
   • Supervisor: Christopher Brix
3. Shared Certificates for Neural Network Verification
   • Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh, Martin Vechev: Shared Certificates for Neural Network Verification
   • Student: –
   • Supervisor: Christopher Brix
4. Detecting Novel Inputs
   • Thomas A. Henzinger, Anna Lukina, Christian Schilling: Outside the Box: Abstraction-Based Monitoring of Neural Networks
   • Student: –
   • Supervisor: Christopher Brix
5. Tricking Novelty Detection Techniques
   • Sara Hajj Ibrahim, Mohamed Nassar: Hack The Box: Fooling Deep Learning Abstraction-Based Monitors
   • Student: –
   • Supervisor: Christopher Brix

B. Compositional Verification of Probabilistic Systems

1. Assume-Guarantee Reasoning
   • Hadar Frenkel, Orna Grumberg, Corina S. Păsăreanu, Sarai Sheinvald: Assume, guarantee or repair: a regular framework for non regular properties, STTT 2022
   • Student: –
   • Supervisor: Hannah Mertens
2. Compositional Strategy Synthesis
   • N. Basset, M. Kwiatkowska, C. Wiltsche: Compositional strategy synthesis for stochastic games with multiple objectives, Information and Computation 2018
   • Student: –
   • Supervisor: Hannah Mertens
3. Circular Assume-Guarantee Reasoning
   • Karam Abd Elkader, Orna Grumberg, Corina S. Păsăreanu, Sharon Shoham: Automated circular assume-guarantee reasoning, Formal Aspects of Computing 2018
   • Student: –
   • Supervisor: Hannah Mertens
4. Compositional Model Checking
   • Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, Sebastian Junges: Pareto Curves for Compositionally Model Checking String Diagrams of MDPs, TACAS 2024
   • Student: –
   • Supervisor: Hannah Mertens

C. Analysis of Partially Observable Stochastic Systems

1. Randomized Value Iteration
   • M. T. J. Spaan, N. Vlassis: Perseus: Randomized Point-based Value Iteration for POMDPs, Artificial Intelligence Research 2005
   • Student: –
   • Supervisor: Alexander Bork
2. Approximate Linear Programming
   • Pascal Poupart et al.: Approximate Linear Programming for Constrained Partially Observable Markov Decision Processes, AAAI 2015
   • Student: –
   • Supervisor: Alexander Bork
3. Almost-Sure Reachability
   • Marck van der Vegt, Nils Jansen, Sebastian Junges: Robust Almost-Sure Reachability in Multi-Environment MDPs, TACAS 2023
   • Student: –
   • Supervisor: Alexander Bork

D. Static Program Analysis for Software Verification

1. Predicate Abstraction (SLAM Tool)
   • Thomas Ball, Sriram K. Rajamani: The SLAM project: debugging system software via static analysis, POPL 2002
   • Thomas Ball, Vladimir Levin, Sriram K. Rajamani: A decade of software model checking with SLAM, Comm. ACM 2011
   • Student: –
   • Supervisor: Thomas Noll
2. Sacrificing Soundness (FindBugs Tool)
   • David Hovemeyer, William Pugh: Finding bugs is easy, ACM SIGPLAN Not. 2004
   • Nathaniel Ayewah, William Pugh, David Hovemeyer, J. David Morgenthaler, John Penix: Using Static Analysis to Find Bugs, IEEE Softw. 2008
   • David A. Tomassi: Bugs in the wild: examining the effectiveness of static analyzers at finding real-world bugs, ESEC/FSE 2018
   • Student: –
   • Supervisor: Thomas Noll
3. Coverity Tool
   • Seth Hallem, Benjamin Chelf, Yichen Xie, Dawson Engler: A system and language for building system-specific, static analyses, PLDI 2002
   • Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler: A few billion lines of code later: using static analysis to find bugs in the real world, Comm. ACM 2010
   • Student: –
   • Supervisor: Thomas Noll
4. Separation Logic (Infer Tool)
   • Peter W. O’Hearn: A Primer on Separation Logic (and Automatic Program Verification and Analysis), Software Safety and Security – Tools for Analysis and Verification, 2012
   • Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O’Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez: Moving Fast with Software Verification, NFM 2015
   • Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O’Hearn: Scaling static analyses at Facebook, Comm. ACM 2019
   • Student: –
   • Supervisor: Thomas Noll
5. Incorrectness Logic (Pulse-X Tool)
   • Peter W. O’Hearn: Incorrectness logic, POPL 2020
   • Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O’Hearn: Finding real bugs in big programs with incorrectness logic, OOPSLA 2022
   • Student: –
   • Supervisor: Thomas Noll

Prerequisites

Basic knowledge in the following areas is expected:

• Formal languages and automata theory
• Mathematical logic

Previous knowledge in semantics of programming languages and program analysis is helpful but not mandatory.

Registration

Registration to the seminar is handled via the SuPra system.

Grading Scheme

You can access the grading scheme here.

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

Additional Material

Contact

Thomas Noll