Seminar Trends in Computer-Aided Verification

Seminar in Theoretical CS, Winter 2024/25

News

  • 06.06.2024: we are online

Dates & Deadlines

TBAKick-off meeting (room 4201b, 2nd floor, building E1, CS Department)
TBATopic preferences due
TBADetailed outline due
TBASeminar report due
TBAPresentation slides due
Jan 20-23, 2025Presentations (room 4201b, 2nd floor, building E1, CS Department)
TBAFinal 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

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
  2. Abstraction-Based Verification with Intervals and Zonotopes
  3. Shared Certificates for Neural Network Verification
  4. Detecting Novel Inputs
  5. Tricking Novelty Detection Techniques

B. Compositional Verification of Probabilistic Systems

  1. Assume-Guarantee Reasoning
  2. Compositional Strategy Synthesis
  3. Circular Assume-Guarantee Reasoning
  4. Compositional Model Checking

C. Analysis of Partially Observable Stochastic Systems

  1. Randomized Value Iteration
  2. Approximate Linear Programming
  3. Almost-Sure Reachability

D. Static Program Analysis for Software Verification

  1. Predicate Abstraction (SLAM Tool)
  2. Sacrificing Soundness (FindBugs Tool)
  3. Coverity Tool
  4. Separation Logic (Infer Tool)
  5. Incorrectness Logic (Pulse-X Tool)

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.

Additional Material

Contact

Thomas Noll