Software and Computational Systems Lab

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:

1. Set up a Database (first locally, then on a server)
2. Identify the relevant information in the witnesses (Size, Creating tool, Verdict, etc.)
3. Setup the Database Schema
4. Make a partial download possible (i.e., download an archive of all witnesses conforming to a query)
5. 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.

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.