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 has not yet achieved its full potential in industrial practice. However, we believe that a scaled CbC approach contributes to solving problems of modern software development. In this tech talk, I will give an overview of our work on CbC in four different lines of research, including developing configurable as well as safety- and security-critical software systems. For all of these, we provide tool support building the CorC ecosystem that facilitates CbC-based development in different fields of application and for differing sizes of software systems.
Ina Schaefer is a full professor of Software Engineering at Karlsruhe Institute of Technology (KIT), Germany. She received a PhD from Technische Universität Kaiserslautern in 2008. She was professor for Software Engineering and Automotive Informatics at TU Braunschweig from 2012-2022. Her main research interests are in the intersection of software engineering and formal methods, particularly focusing on correctness-by-construction development and quality assurance for software-intensive and variant-rich systems.
