Useability of the Tool CorC Using Artificial Intelligence

  • 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.

     

    Goal: In this thesis, AI-tool support that improves the useability and understanding for unexperienced developers 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. Further, the integration should be evaluated regarding the improvement for developers as well as the correctness of the results of the selected AI-model.

     

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