Motivation

Software verification tools such as CPAchecker are becoming increasingly effective in proving the correctness of C programs or detecting programming errors. Albeit their effectiveness, there are still surprisingly small programs where these sophisticated verifiers fail or time out. The cause of failure in most cases is still unclear today and can possibly be attributed to a complex interaction of programming language features (e.g. nested loops together with pointers and arrays). 
Without a clear intuition, advancing existing verifiers becomes highly difficult.

Goals

During the thesis, the first steps towards uncovering the root cause of difficulties for common verification tools should be taken. The starting point are simplistic
C programs with a clear and human-verifiable verification goal. Then, the verification complexity should be iteratively increased by so called identity transformations.
An identity transformation injects code that do not change 
the program semantic but increase the verification difficulty (possibly by introducing new language elements). An example for such a transformation could be: 

int a = 5; -- T --> int a; int b = 5; a = b; 

It is possible to choose this topic for a bachelor or master thesis.

In the context of a bachelor thesis, the following goals should be achieved:
- the development of general framework to apply identity transformation on
   C code (e.g. via String matching)
- the implementation of a set of simple identity transformations
   that support central features of the C language
- Producing and evaluating on a small generated benchmark for the software verification tool CPAchecker

In the context of a master thesis, the goals are extended to:
- the development and implementation of more complex identity transformations
   (e.g. by transforming the program AST)
- a larger set of hand-crafted benchmarks used for transformations
- a large-scale evaluation on a generated benchmark with at least three state-of-the-art verification tools

Contact: ,

Motivation:
The goal of software verification is to prove or disprove whether a program satisfies a given specification. In doing so, many approaches explore the state space of the program or generate predicates to abstract the state space. In the case of a faulty program, however, many existing techniques tend to waste time exploring correct parts of the program.  Adjusting the search strategy or switching to a different verification algorithm could be beneficial in these cases. With the help of machine learning, we aim to design an algorithm that detects these situations during verification.

Goal:
Collecting relevant data and generating a meaningful dataset is an essential part of data-driven algorithms. Therefore, the goal of this work is to automatically generate a dataset for learning verification behaviors.The goal of the thesis is to develop and implement a technique to analyze the search behavior or the predicates generated by a verification algorithm, identify relevant events, and store the collected information in a suitable format.The developed approach shall then be integrated into the verification framework CPAchecker[1], which also provides the necessary verification algorithms. Ultimately, the novel technique will be used to generate a dataset, while the performance and quality of the generation process will be evaluated. Simple decision rules for predicting the probability of success will also be defined.

It is also possible to work on the topic for a master's thesis. In this case the data generation is only the first part. In a second part, a machine learning algorithm shall be developed to predict the success probability of the current verification. The learning algorithm will then be evaluated in terms of accuracy and runtime.

Contact: