Ina Schaefer on X-by-Construction

Could you introduce yourself and your research area?

My name is Ina Schaefer, and I have been a professor of software engineering at KIT, since April 2022. Formal methods are very close to my heart, and that is still the part of my research that excites me most.

In my group, we broadly work in three main research areas: The first is to improve the scalability and applicability of formal methods, mainly by using principles of compositionality and the development of tools. The second is quality assurance for software via principled software testing approaches, mainly for variant-rich, configurable and evolving software. The third is quantum software engineering, where we strive towards applying software engineering principles and formal methods for the development of software for quantum computers.

What are the most exciting current advances in your research field?

I guess, most would expect me to say that the most exciting current advances are AI and LLMs. But I must admit that I am not super excited about AI even though it is of course stunning what AI-based systems can achieve and that kind of texts LLMs can produce. Maybe my lack of excitement comes from the fact that as an undergrad student I worked at the German Institute for AI (DFKI Saarbrücken), and I was actually doing formal methods and program verification, which were still considered to be AI at that time. And maybe, I am just somewhat sad that AI is currently reduced to statistical learning only and that the older branches of AI such as theorem proving and formal methods are temporarily out of fashion.

So actually, I am most excited about correctness-by-construction (CbC) as a software development paradigm. I believe that we can build much better software than we currently do, if only we applied the development principles that we already know. And CbC is indeed one of those principles that my group and I together with a number of collaborators have been working on for roughly the past 10 years with the goal to provide more tool support and automation and to design approaches that make CbC scale to larger classes of systems and properties, such as software product lines and security properties beyond plain functional correctness. A recent exciting project is the development of Quantum-by-Construction, a CbC-based development approach for quantum programs, that may help us also in finding novel quantum algorithms if quantum software development becomes more rigorous. Of course, we are also experimenting with LLMs to ease the use of CbC-based development, and the results are promising.

What do you expect will be the next big thing/challenge in this field?

For me, the next challenge in correctness-by-construction engineering is to extend the approach to the constructive development of software not only satisfying functional correctness properties by also other non-functional properties at the same time. We called this approach X-by-construction a couple of years ago—where X stands for any non- or extra-functional property. At that time, XbC was mainly a buzzword, though. But very recently, we have started working on approaches for constructing programs with guarantees on their resource consumption, e.g., energy or memory consumption. Once we have XbC development approaches for a number of relevant X-properties, my vision is to support taxonomization of algorithmic families, i.e., program variants all satisfying the same functional specification, but differing in their non-functional properties, to allow for informed trade-off decisions for the most suitable algorithmic variant with respect to its non-functional characteristics with build-in guarantees on both functional and non-functional behaviour.

That sounds very interesting! Can you elaborate a bit on the methodological differences and the challenges involved in reasoning about X-by-construction as opposed to correct-by-construction?

For functional CbC, we use state-based pre-/post-condition specifications, as we know them, e.g., from method contracts, and refinement rules as we know them for Hoare logic. For each program construct that we introduce, the refinement rules generate a set of local side conditions that we verify using existing functional program verifiers. For XbC, things are more tricky: first, we need to be able to specify the X-properties that we are interested in. This can be non-trival (and maybe even impossible for some types of properties) as we have to find a specification formalism that is capable to express often quantitative non-functional properties in a local and modular manner. Second, we have to find refinement rules that allow us to introduce program statements and transform the X-property specifications in a way that preservers their validity subject to side conditions. Third, we need appropriate reasoning methods (decision procedures, verifiers, etc.) to establish the side conditions of the refinement rules which may be quantitative constraints as the X-property specifications.

Can you tell us a bit about the DFG (German Research Foundation) Priority Programme on quantum software engineering that you recently (co)initiated?

As a spin-off from my initial goal to develop Quantum-by-Construction, I got involved with the quantum software engineering community. With a number of colleagues from different fields of computer science all interested in quantum computing, we initiated a DFG Priority Programme focussing on algorithms, methods and tools for the quantum software stack. The field of quantum computing is still very much physics-driven and hardware-oriented as the quest for the best hardware platform for quantum computing is still ongoing. However, we strongly believe that once that quest for quantum computing hardware is ending, value in quantum computing will be created by the software running on the quantum hardware, as in classical computing. Thus, the goal of the priority program is to foster fundamental and methodological research along all levels of the quantum software stack, including quantum algorithms, quantum programming languages and compilers, middleware and operating systems for quantum computing, design methods for quantum computing hardware and also verification and validation of quantum software.

What advice would you give to someone just starting their career in research?

My advice is to not follow the current fashions in research, as they might change quickly. Rather find and work on something that really interests you and that you (personally) find relevant! That will allow you to go the extra mile when needed and to deal with the frustrations when a paper or a proposal is rejected.

Do you think the AI trend will fade, though?

I am not sure, I think AI is here to stay, but I hope that the AI hype will die down shortly, and I hope that we get more aware of what AI can really do, where the risks and limitations are, and where it can really complement tasks that we are doing.

Finally, who would you like to see interviewed on the ETAPS blog?

Of course, there are senior people in the formal methods field that were my “heros” when I was a PhD student, and I am kind of guessing you are asking about those names here… but honestly, I would rather like to see junior people, female researchers, people from the Global South and overall people bringing more diversity to the community being interviewed to show that formal methods is a striving and innovative research field.

And which paper would you recommend everyone to read?

I would rather like to recommend a book that I recently read, and this is Nexus by Harari. In this book, Harari explains how the way we distribute information in social networks determines the governance structure of a society and how the advent of AI, or alien intelligence as Harari calls it, transforms those societies…