Formal Specifications in CbC Engineering 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 WebCorC offers possibilities to develop programs using CbC and to verify their correctness. At the moment, users are required to define specifications and Java-code manually.

     

    Goal: The goal of this Bachelor thesis to exploratively define a prompt for generating formal specifications from natural language descriptions in the tool WebCorC. We are aiming to use a benchmark of formal specifications which is translated into natural language. This natural language specifications are to be formalized using LLMs and checked regarding equivalence to the original formal specifications. During this process, the prompts are to be refined incrementally until achieving satisfing results.

     

    Requirements: Experience in promt engineering of advantage but not mandatory.