We are hiring new student research assistants and tutors. Apply now!
Paper accepted at ICSE 2023: "CoVeriTeam Service: Verification as a Service"

Dr. Philipp Wendler

Akademischer Rat

Picture of Dr. Philipp Wendler

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 008, Oettingenstr. 67
Office hours
Monday 10-11 please contact via e-mail
+49 89 2180-9181
lastname @ sosy.ifi.lmu.de
Personal Homepage


Please send me encrypted mails!
My GPG key: 0x31A9DE8C
Fingerprint: 19D5 A10B 2D97 88D8 7CBE E5ED 62C0 F78C 31A9 DE8C

Thesis Mentoring

Available topics
Support for exceptions in the Java analysis of CPAchecker
Refinement Selection with Adjustable-Block Encoding [1, 2, 3]
Currently assigned topics
Data Flow Based Assessment of Unintended Test Result Deviations

Background: Unintended Test Result Deviations (UTRD) denote changes in test results that are not due to changes in the code under test. UTRD constitute a major impediment to regression testing (a corner-stone of modern software development), because a change in test results is commonly attributed to a change in the code under test (CUT). If a test verdict changes due to other reasons, developers may waste time debugging the CUT, which is not the cause of the changed test result. UTRD has been acknowledged as a major problem by major software companies and organizations, including Microsoft, Google, and Mozilla.
Goal: The goal of the proposed thesis is to develop a static data-flow analysis to detect whether test outcomes, which are usually based on data comparisons, depend on possibly uncontrolled inputs to the CUT. Such uncontrolled inputs may, for instance, be environment variables, file I/O, usage of random number generators, etc. The analysis is supposed to work on C programs and should be based on the CPAchecker framework.

Consolidate pointer-aliasing analyses in CPAchecker [1]

CPAchecker has several different implementations of pointer-aliasing analyses, and the current state of what they support is unclear. This leads to the fact that they are rarely used and causes wrong results in case of pointer aliasing. The goal of this thesis is to create a strong CPA for pointer aliasing (either by merging the existing CPAs or rewriting them) that supports all necessary use cases (fast and imprecise as well as more precise) and migrate all existing uses of other pointer CPAs, such that the old code can be deleted (#358). Afterwards, it may be possible to add additional features (e.g., #742) or extend other components of CPAchecker to make use of the new CPA (e.g., #527, #398).

Byte-level heap of predicate analysis CPAchecker [1, 2, 3]

CPAchecker currently models a program's heap as arrays of ints/floats/etc., depending on the types used in the program (cf. Section 4.4.3 of [3]). This is imprecise and prevents us from supporting functions like memset, which treat memory as an array of bytes. The goal of this project is to add an alternative heap encoding to CPAchecker's predicate analysis that allows byte-wise access to the heap and support for memset/memcpy/etc.

Extend allocation of CPU cores in BenchExec [1, 2]

BenchExec is a benchmarking framework and assigns a specific set of CPU cores to each benchmark run. The calculation which core to use for which run needs to consider low-level details of the hardware architecture (like hyper threading, NUMA, etc.) in order to avoid interference between runs as far as possible. Our current implementation supports multi-CPU systems with NUMA and hyper threading, but not some more recent features like hybrid-architecture CPUs or CPUs with split Level 3 caches. The goal of this thesis is to implement a more general core allocation (in Python) with support for all kinds of modern CPUs and additional features and rigorous tests. There should also be an experimental evaluation on how different allocation strategies and such hardware details influence benchmarking results.

Finished topics
String analysis in CPAchecker [1, 2]
String analysis in CPAchecker [1, 2]
LTL software model checking
A JavaScript frontend for CPAchecker
Improve analysis of Java programs in CPAchecker
Towards understandability of verification result: visualization of graphs produced by verifiers
Predicate analysis based on splitting states for CPAchecker [1, 2]
Improve predicate analysis based on domain-type of variables in CPAchecker [1, 2]
New Approaches and Visualization for Verification Coverage [1]
Good, bad, ugly interpolants. Measure interpolants and build heuristics. Topic might be related to refinement selection. [1]
Use cgroups v2 for BenchExec to improve container isolation [1, 2]

Our benchmarking framework BenchExec uses cgroups in order to limit and measure time and memory usage during benchmarking. The Linux kernel is replacing cgroups with a new API (v2) and we need to support this in BenchExec (#133). Once we have it, we can use cgroup namespaces to better isolate our containers and provide full support for nested containers (#436).

Modern architecture and tests for HTML tables of BenchExec [1]
Improve usability of summary tab for HTML tables of BenchExec [1]

If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.



(List at DBLPMy ORCID)

Other Responsibilities