Seminar Topics: Winter Semester 2017/18

Back to Seminar page

The list below is not final yet. Topics will still be added or removed, supervisors might change, but the list below might give you an idea of what you can expect in the seminar.

Please note that PDFs for some papers are only accessible via the university network.

Bachelor Topic Supervisor
SMT solvers Sebastian Schweizer
Generating verification conditions Sebastian Schweizer
The Dafny and Boogie verification tools Mathias Weber
The Chalice verification tool Peter Zeller
Property based testing Mathias Weber
Concolic testing Peter Zeller
Model checking Peter Zeller
Master Topic Supervisor
QUELEA Peter Zeller
TLA+ Mathias Weber
Concuerror Annette Bieniusa
Session Types Sebastian Schweizer
Rules-Based Programming Arnd Poetzsch-Heffter
The Blockchain Deepthi Akkoorath
ACIDRain Deepthi Akkoorath
Serializability for eventual consistency Arnd Poetzsch-Heffter
MOLLY Annette Bieniusa
Generalized Isolation Level Definitions Deepthi Akkoorath
Client-Centric Specification of Database Isolation Annette Bieniusa

Bachelor

SMT solvers

The goal of this seminar topic is to explain the basic architecture of SMT (Satisfiability modulo theories) solvers and illustrate a use case for an SMT solver based on an example.

Generating verification conditions

SMT-solvers can be used to verify the correctness of programs. To do this, programs with their specification have to be translated into logical formulas. The goal of this topic is to explain how this can be done by calculating “weakest preconditions”.

The Dafny and Boogie verification tools

In this topic the concrete verification tool “Dafny” (and its backend “Boogie”) should be presented. The focus here should be on explaining how the a concrete tool can be used to verify program. In particular the verification of programs with loops and procedures shall be explained using suitable examples.

The Chalice verification tool

Chalice is a programming language and program verifier for concurrent program. The focus for this seminar should be on explaining the techniques used by Chalice for verifying concurrent programs, in particular the concepts of framing and permissions.

Property based testing

The goal of this topic is to explain, how a specification can be checked through testing instead of verification. This shall be explained based on the Haskell libraries “QuickCheck” and “SmallCheck”, which use random testing and bounded enumeration of inputs.

Concolic testing

This topic is about a smarter approach to property based testing, where different inputs are explored using symbolic executing. The goal here is to explain symbolic execution and how it is used to explore different executions of the program in testing.

Model checking

For this topic, the basics of model checking should be explained. In particular, it should be explained, how model checking can be used to verify programs using the Java PathFinder tool as an example.

Master

QUELEA

TLA+

Concuerror

Session Types

The goal of this seminar topic is to explain the basic ideas of session types based on the language Scribble.

Rules-Based Programming

The Blockchain

The goal here is to explain the protocol behind Blockchains, which are used in crypto-currencies such as Bitcoin. Moreover the distinction between Proof-of-Work vs. BFT replication should be explained and usages of Blockchain protocols beyond crypto-currencies should be researched and explained.

ACIDRain

Serializability for eventual consistency

MOLLY

Generalized Isolation Level Definitions

Client-Centric Specification of Database Isolation