Stud.IP Uni Oldenburg
University of Oldenburg
04.03.2024 08:53:52

Personal details

Title 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.
Home institution Department of Computing Science
Type of work practical / application-focused
Type of thesis Bachelor's
Author Cedric Richter
Status available
Problem statement
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 (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.
Created 29/01/24

Study data

  • Formale Methoden
Degree programmes
  • Dual-Subject Bachelor's Programme Computing Science
  • Bachelor's Programme Computing Science
Assigned courses
Contact person