|Safer code generation with ChatGPT and Formal Verification
Large Language Models (and ChatGPT in particular) are becoming increasingly effective at generating program code. Unfortunately, however, code generation is not always error-free, which can lead to bugs or security vulnerabilities in the generated code. This can have serious consequences, especially in safety-critical systems.
Most existing approaches try to prevent this by developing tests for the generated code or having them developed (using another language model). However, testing can only detect errors, but cannot show that code is error-free. For this reason, we want to take the first step in this bachelor thesis to evaluate whether formal verification can be used to verify the results of code generation.
|Department of Computing Science
|Type of work
|practical / application-focused
|Type of thesis
The idea is to automatically generate formal specifications for a generation problem and then check them using a formal verification tool.
Typically, generation problems consist of a natural language description together with a set of tests. The large language model then generates code that should correspond to the description.
The goal of the bachelor thesis is to develop an approach to generate formal specifications based on the natural language description (and the tests) using ChatGPT. The bachelor thesis focuses on generation problems in C and we use state-of-the-art verification tools to evaluate the generated specification.
Translated with DeepL.com (free version)
The Bachelor thesis can be written in either English or German. However, a good knowledge of English is a must for interacting with ChatGPT. Good programming skills in Python (for tool development) and/or C would be an advantage.