Automatically Engineering Trusted Software: A Research Roadmap

Recent advances in automated programming have the potential to reduce human involvement in the software engineering process, but this can lead to less trustworthy software. We envision a three-pronged approach to automating the engineering of trustworthy software that involves (1) eliciting requirements from users and automatically generating formal specifications encoding users’ intent, (2) automatically synthesizing source code conforming to those specifications, and (3) automatically synthesizing formal proofs to verify the correctness of the produced software. We describe this vision and the state of the art in each of these three areas, and the research challenges that must be overcome in each area and in their integration.