Towards AI-assisted Correctness-by-Construction Software Development

@InProceedings{kodetzkiBordisKirstenSchaefer2024,
  title        = {Towards AI-assisted Correctness-by-Construction
                  Software Development},
  author       = {Maximilian Kodetzki and
                  Tabea Bordis and
                  Michael Kirsten and
                  Ina Schaefer},
  year         = {2025},
  month        = oct,
  booktitle    = {12th International Symposium on Leveraging Applications of
                  Formal Methods, Verification and Validation ({ISoLA} 2024).
                  Software Engineering Methodologies},
  venue        = {Crete, Greece},
  eventdate    = {2024-10-27/2024-10-31},
  series       = {Lecture Notes in Computer Science},
  editor       = {Tiziana Margaria and
                  Bernhard Steffen},
  publisher    = {Springer},
  abstract     = {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.},
  pages        = {222--241},
  doi          = {10.1007/978-3-031-75387-9_14}
}