Correctness-by-Construction Engineering - Can we build better software?
Session Chair: Silvia Lizeth Tapia Tarifa
Correctness-by-Construction (CbC) is an incremental software development technique to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification mainly take part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules. This specification-first approach has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged many years ago, CbC is not widespread and is mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software development. In this keynote, I will give an overview of our work on CbC in four different lines of research. For all of them, we provide tool support building the CorC ecosystem that even further enables CbC-based development for different fields of application and sizes of software systems.