Software and Computational Systems Lab

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.