Towards AI-Assisted Correctness-by-Construction Software Development

In recent years, research on artificial intelligence (AI) has made great progress. AI-tools are getting better in simulating human reasoning and behavior every day. In this paper, we discuss the extent to which AI-tools can support Correctness-by-Construction (CbC) engineering. This is an approach of formal methods for developing functionally correct programs incrementally on the basis of a formal specification. Using sound refinement rules, the correctness of the constructed program can already be guaranteed in the development process. We analyze the CbC process regarding steps for potential AI-tool support in the tool CorC, which implements CbC. We classify the findings in five areas of interest. Based on existing work, expert knowledge, and prototypical experiments, we discuss for each of the areas whether and to what extent AI-tools can support CbC software development. We address the risk of AI-tools in formal methods and present our vision of AI-integration in the tool CorC to support developers in constructing programs using CbC engineering.