© FZI
Unifying Speaker Ina Schaefer
Prof. Dr. Ina Schaefer is a full professor at the Karlsruhe Institute of Technology (KIT) since April 2022 and heads the “Test, Validation and Analysis of Software-Intensive Systems (TVA)” research group at the Institute for Information Security and Dependability (Institut für Informationssicherheit und Verlässlichkeit – KASTEL).
Previously, she was a professor of Software Engineering and Automotive Informatics at the TU Braunschweig. She did her doctorate in October 2008 at the TU Kaiserslautern. Ina spent her PostDoc period from September 2009 to October 2010 at Chalmers University of Technology in Gothenburg, Sweden.
The focus of her research is the integration of formal methods into software development and correctness-by-construction engineering so that software can become better than it currently is. Ina is particularly interested in aspects of scalability, modularity, and reusability. Applications for this work can be found in a variety of systems, including automotive, aviation, and automation, and quantum computing.
She co-leads the Mobility Lab in the Helmholtz Engineering Secure Systems program and is Vice Dean of the Department of Computer Science at KIT. Since 2022, she is Co-Chair of the Expert Committee “Transformation of the Automotive Industry” at the German Federal Ministry for Economics and Climate Action.
Talk
Correctness-by-Construction—Past, Present and Future
Time: TBA
Room: TBA
Correctness-by-Construction (CbC) engineering is complementary to traditional post-hoc analysis and verification techniques. Instead of writing a program and then most likely showing that it is incorrect, CbC engineering starts from a specification of the desired program properties and through a sequence of sound refinements obtains a program that by-construction satisfies its specification. In the past, CbC was mainly a paper-and-pencil exercise taught to students of introductory programming. Recently, it has gained traction towards becoming an engineering approach for highly safety- and mission-critical software.
In this keynote talk, I describe the roots of CbC and its early protagonists in the past. For the present, I discuss our efforts to scale CbC to a rigorous software development approach by providing user-directed tool support integrating CbC into modern software development processes. This includes more lightweight correctness guarantees as well as AI-support during CbC development. For the future, I report on exciting avenues for CbC: first, QbC, the application of CbC for functional correctness of quantum programs, and second, X-by-Construction (XbC), the application of CbC principles to programs that are not only functionally correct, but also have guarantees on specific non-functional properties (the “X”).