Henrik Wachowitz
Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538
Munich
(Germany)
- Office
- Room F 006, Oettingenstr. 67
- Office Hours
- Mi. 13-14h, Do. 13-14h (please notify if you plan to visit)
- firstname.lastname@ifi.lmu.de
- ORCID
-
0000-0002-4768-4054
GPG-Key
Please send me encrypted mails!
My GPG key: 0xECB49A11554D9130
Fingerprint: A3B3 86DE ACD4 6C1F 618B 31F2 ECB4 9A11 554D 9130
Thesis Mentoring
Available topics
WitnessDB: Storing, Querying, and Analyzing Verification Witnesses [1]
Verification Witnesses are the result of a Software Verification run. They contain information that should make reproducing the TRUE or FALSE verdict of a given program easier. The annual international competition for software verification SV-COMP produces a large number of these witnesses from a plethora of verification tools. There is one drawback however: the dataset is only available as a large ZIP archive. When unpacked, the archive of just SV-COMP ’24 is already 100 GB in size.
In this Project you will build migrate these witnesses to a Database to make them queryable. The task will require you to:
- Set up a Database (first locally, then on a server)
- Identify the relevant information in the witnesses (Size, Creating tool, Verdict, etc.)
- Setup the Database Schema
- Make a partial download possible (i.e., download an archive of all witnesses conforming to a query)
- Create a Web Interface to query the Database
Applicants should have experience with SQL, Databases and be proficient in one of Python, Java, Kotlin, Go or C++ as well as have some experience with web technologies. Experience with Docker/Podman and Web Development is a plus.
Currently assigned topics
An IDE Plugin for Software Verification
This topic is available as a BSc thesis or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.
Goal: We integrate the program-analysis tool CPAchecker into IDEs like VSCode and IntelliJ by building a language server for it.
Background: CPAchecker is a powerful tool for program analysis and formal verification. It automatically finds errors in code. But currently, CPAchecker only has a command-line interface. To make it easier to use CPAchecker during development, we want to integrate it into IDEs. Traditionally, a separate IDE plugin had to be written for each IDE that we want to support, but the language server protocol provides one protocol that allows us to integrate CPAchecker into a variety of IDEs by building a single language server.
Details: You build a language server for CPAchecker and the C programming language. The server receives requests from IDEs that contain program code. The server then runs CPAchecker on that code and responds to the IDE with a list of found issues. A basic web service for communicating with CPAchecker already exists and can be used in the backend. The goal is to be able to both deploy the language server locally and remotely (e.g., in the cloud).
Knowledge in software verification is helpful. An understanding of Java micro-services is helpful. The language server should be written in Java.
In the scope of this topic, you have to create a design of the language server, implement this design, and test the server.
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.