Automated Generation of Formal Specifications and Java-code Using Artificial Intelligence in the Tool CorC

  • 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. At the moment, users are required to define specifications and Java-code manually.

     

    Goal: In this thesis, AI-tool support that can generate formal specifications based on a description in natural language, as well as Java-code based on a formal specification, should be integrated and evaluated in CorC. The thesis consists of a comparison of existing AI-models and the integration of one of the models. The integration should be evaluated reagrding the correctness and reliability of the results of the selected AI-model.

     

    Requirements: Programming knowledge in Java, basic knowledge in the area of formal specifications is an advantage, knowledge in AI-tools is an advantage