3 Papers accepted at ISoLA'20: "An Interface Theory for Program Verification", "Verification Artifacts in Cooperative Verification", and "Violation Witnesses and Result Validation for Multi-Threaded Programs"

Dr. Philipp Wendler

Akademischer Rat

Picture of Dr. Philipp Wendler

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]
Partial Predicate Abstraction [1, 2, 3]
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]
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.

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
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