Synthesizing CbC Programs From Formal Specifications using LLMs

  • Context: Correctness-by-Construction (CbC) is a method for software development. In this process, programs are contracted and created through correctness-preserving refinements. The tool CorC offers possibilities to develop programs using CbC and to verify their correctness. However, using CorC requires knowledge and experience in formal specifications and formal verification. Previous work has shown potential in supporting the CbC development process by using LLMs to automatically generate formal specifications from natural language and Java code from formal specifications. 

    Goal: The goal of this thesis is to combine the existing approaches to a holistic technique for synthesizing complete CbC programs from a formal or natural language input. The goal is to automatically derive specifications, code, and, especially, refinement steps using large language models. The thesis will contain conceptual work on prompt engineering and a literature study on existing techniques. The concepts are to be evaluated as empirical study using different LLMs that have shown potential in previous work.

    Requirements: Programming knowledge in Java, basic knowledge in the area of program verification and specification, knowledge in AI-tools is an advantage.