Safeguarding AI-Based Software Development and Verification using Witnesses (Position Paper)

Abstract

This position paper accompanies a presentation and discussion at AISoLA 2023 on the topic of how (generative) AI influences software engineering, namely, the development and verification of software programs. We outline a few opportunities and challenges that are posed by the application of AI. AI-based techniques can be an efficient method to produce software code. Not only this, AI can also be efficient in producing invariants that help proving correctness of software programs. But unfortunately, the results generated by AI-based approaches are often still imprecise or wrong: Code produced with the help of AI often does not satisfy the specification, and AI-generated invariants are often not helpful to prove the correctness of the program. The solution is to safeguard the process by independently checking the results using verification witnesses and witness validation. The goal of this paper is to convince readers that software witnesses are important and that independent result validation is of utmost importance to ensure correctness.