Dr. Philipp Wendler, LMU Munich

Dr. Philipp Wendler

Akademischer Rat

Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Office: Room F 008, Oettingenstr. 67
Office hours: ~~Monday 10-11~~ please contact via e-mail
Phone: +49 89 2180-9181
E-Mail: firstname.lastname@lmu.de
Personal Homepage: https://www.philippwendler.de

GPG-Key

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

Thesis Mentoring

Available topics

Refinement Selection with Adjustable-Block Encoding [1, 2, 3]

Heuristics for Selecting Predicates for Partial Predicate Abstraction [1]

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.

Currently assigned topics

Improve analysis of Java programs in CPAchecker

Improve predicate analysis based on domain-type of variables in CPAchecker [1, 2]

Verification Coverage: what parts of a program are covered by a verifier? [1]

Improve usability of summary tab for HTML tables of BenchExec [1]

Finished topics

String analysis in CPAchecker [1, 2]

LTL software model checking

A JavaScript frontend for CPAchecker

Support for exceptions in the Java analysis of CPAchecker

Towards understandability of verification result: visualization of graphs produced by verifiers

Predicate analysis based on splitting states for CPAchecker [1, 2]

Good, bad, ugly interpolants. Measure interpolants and build heuristics. Topic might be related to refinement selection. [1]

Modern architecture and tests 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.

Projects

Publications

(List at DBLP – My ORCID)

Other Responsibilities

Employee Representative in the steering committee of the Institute of Informatics at LMU