Research

Our research aims at developing concepts, methods, and tools for the holistic engineering of reliable and secure software-intensive systems. These software systems must be robust and resilient to planned and unplanned changes in the context of configuration, reconfiguration, or evolution. The systems must be reliably and securely dynamically adaptable to new application scenarios and environments and support systematic reuse. In this context, precise, mathematically sound guarantees for critical functional and non-functional system properties, especially for reliability and security, are essential. Application areas for this research are primarily in automotive software and systems engineering and in automation engineering in mechanical and plant engineering.

Research topics

  • Security-by-Design and By-Construction Engineering:
    Software-intensive systems in safety and mission-critical areas place high demands on their safety (safety and security) and reliability. These essential system properties must already be taken into account in the development process in order to be able to guarantee them in operation. The approach of by-construction engineering aims at developing software systems starting from a (formal) specification of their functional and non-functional properties in such a way that they fulfill these properties by construction.
  • Software Diversity (Variability & Adaptability): Modern software systems are highly configurable to adapt to different requirements and environmental conditions. This configurability at development time can also be used as adaptability at runtime, allowing systems to self-adapt to new conditions. This can improve the robustness and resilience of software systems through diversity, which can be used in particular to harden systems against attacks.
  • Provable Security and Post-hoc Quality Assurance:
    Complementary to by-construction engineering, post-hoc quality assurance techniques aim to test critical functional and non-functional properties of systems, including reliability and security, to ensure the quality of these systems. A particular focus of research is on efficient and effective test procedures based on systematic test case generation, test case selection, and test case prioritization, especially for variant and evolving software systems. This also includes assurance procedures for intelligent systems, where parts of the functionality are realized by trained AI components. A current research project is concerned with end-to-end testing of intelligent driving functions in the context of automated driving, which should also detect targeted attacks on the AI components. Another research focus is the use of formal methods, in particular deductive verification, for the quality assurance of software systems. In this context, our research aims at scaling these techniques by exploiting modularity and improving usability through modern AI-based methods.
  • Legacy Software Analysis:
    Modern software systems are generally no longer developed from scratch. Instead, software systems are continuously evolving. However, this continuous development often leads to the loss of documentation about the software systems as well as the transfer of errors from one part of the system to another by copying. Research in the area of legacy system analysis aims to analyze existing structures of these systems (re-engineering) and thus create opportunities to restructure or even migrate the legacy systems. For example, existing functionalities of a legacy system can be transferred into a new type of security architecture. The extraction of reusable building blocks from legacy systems enables a systematic reuse and further development of these systems with the goal of Sustainable Software Engineering.
Projects
Title Contact

Tim Bittner, Joshua Ammermann, Ina Schaefer

Domenik Eichhorn, Ina Schaefer

Lukas Birkemeyer, Ina Schaefer

Tobias Pett, Ina Schaefer

Tabea Bordis, Maximilian Kodetzki, Rasmus Ronneberg, Ina Schaefer

Publications


Towards AI-Assisted Correctness-by-Construction Software Development
Kodetzki, M.; Bordis, T.; Kirsten, M.; Schaefer, I.
2025. Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies – 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part IV. Ed.: T. Margaria, 222–241, Springer Nature Switzerland. doi:10.1007/978-3-031-75387-9_14
Model-Based Testing of Quantum Computations
Lochau, M.; Schaefer, I.
2025. Tests and Proofs : 18th International Conference, TAP 2024, Milan, Italy, September 9–10, 2024, Proceedings, Ed.: M. Huisman, F. Howar, 127 – 147, Springer Nature Switzerland. doi:10.1007/978-3-031-72044-4_7
Family-Based Vulnerability Discovery for Software Product Lines. master’s thesis
Bächle, T.
2024, November 28. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000177489
Consistency in Cross-Generational Engineering of Cyber-Physical Systems
Albers, A.; Schaefer, I.; Gesmann, L.; Ochs, P.; Fischer, M.; Pett, T.; Schwarz, S. E.
2024. DS 133: Proceedings of the 35th Symposium Design for X (DFX2024). Ed.: D. Krause, 085–094, The Design Society. doi:10.35199/dfx2024.09
MulTi-Wise Sampling: Trading Uniform T-Wise Feature Interaction Coverage for Smaller Samples
Pett, T.; Krieter, S.; Thüm, T.; Schaefer, I.
2024. SPLC ’24: Proceedings of the 28th ACM International Systems and Software Product Line Conference - Volume B. Ed.: M. Cordy, 47–53, Association for Computing Machinery (ACM). doi:10.1145/3646548.3672589
Implementing a System Generation Aware Unified Conceptual Model. bachelor’s thesis
Rak, L.
2024, May 17. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000174678
Quantum Solution for Configuration Selection and Prioritization
Ammermann, J.; Brenneisen, F. J.; Bittner, T.; Schaefer, I.
2024. Proceedings of the 5th ACM/IEEE International Workshop on Quantum Software Engineering, 21–28, Association for Computing Machinery (ACM). doi:10.1145/3643667.3648221
Explaining Edits to Variability Annotations in Evolving Software Product Lines
Güthing, L.; Bittner, P. M.; Schaefer, I.; Thüm, T.
2024. VaMoS ’24: Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems, 93–102, Association for Computing Machinery (ACM). doi:10.1145/3634713.3634725
Sampling Cardinality-Based Feature Models
Güthing, L.; Weiß, M.; Schaefer, I.; Lochau, M.
2024. VaMoS ’24: Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems, 46 – 55, Association for Computing Machinery (ACM). doi:10.1145/3634713.3634719
Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines
Kodetzki, M.; Bordis, T.; Runge, T.; Schaefer, I.
2024. VaMoS ’24: Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems. Ed.: T.Kehrer, 17–26, Association for Computing Machinery (ACM). doi:10.1145/3634713.3634714
Glaubwürdigkeit von Software-in-the-Loop-Testsystemen: Potentiale und Herausforderungen
Kieneke, A.; Schenkel, P.; Pett, T.; Langner, J.; Ecin, O.; Schaefer, I.
2024. 9th AutoTest Technical Conference, Stuttgart, 16th-17th October 2024, FKFS Forschungsinstitut für Kraftfahrwesen und Fahrzeugmotoren
Integrated Approach for High-quality Software Development of Upgradeable Vehicles
Schindewolf, M.; Kuebler, M.; Pett, T.; Hettich, L.; Agh, H.; Lorenz, J.; Wagner, S.; Weyrich, M.; Schaefer, I.; Düser, T.; Sax, E.
2024. 2024 Stuttgart International Symposium on Automotive and Engine Technology – Teil 2, Hrsg.: A. Kulzer, 202–217, Springer Vieweg. doi:10.1007/978-3-658-45010-6_13
Consistency in the View-Based Development of Cyber-Physical Systems (Convide)
Reussner, R.; Schaefer, I.; Beckert, B.; Koziolek, A.; Burger, E.
2023. 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), Västerås, Sweden, 01-06 October 2023, 83–84, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/MODELS-C59198.2023.00026
SOTIF-Compliant Scenario Generation Using Semi-Concrete Scenarios and Parameter Sampling
Birkemeyer, L.; Fuchs, J.; Gambi, A.; Schaefer, I.
2023. 2023 IEEE 26th International Conference on Intelligent Transportation Systems (ITSC), 2139–2144, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ITSC57777.2023.10422637
Is Scenario Generation Ready for SOTIF? A Systematic Literature Review
Birkemeyer, L.; King, C.; Schaefer, I.
2023. 2023 IEEE 26th International Conference on Intelligent Transportation Systems (ITSC), 472–479, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ITSC57777.2023.10422664
Quantum Computing for Feature Model Analysis – Potentials and Challenges
Eichhorn, D.; Pett, T.; Osborne, T.; Schaefer, I.
2023. SPLC ’23: Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A, Ed.: P. Arcaini, 1 – 7, Association for Computing Machinery (ACM). doi:10.1145/3579027.3608971
Continuous T-Wise Coverage
Pett, T.; Heß, T.; Krieter, S.; Thüm, T.; Schaefer, I.
2023. SPLC ’23: Proceedings of the 27th ACM International Systems and Software Product Line Conference. Vol. A. Ed.: P. Arcaini, 87–98, Association for Computing Machinery (ACM). doi:10.1145/3579027.3608980
True Variability Shining Through Taxonomy Mining
König, C.; Rosiak, K.; Cleophas, L.; Schaefer, I.
2023. Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A, 182–193, Association for Computing Machinery (ACM). doi:10.1145/3579027.3608989
Combined Modeling of Software and Hardware with Versions and Variants. master’s thesis
Ochs, P.
2023, August. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000165923
Correctness-by-Construction – Wie machen wir bessere Software? (Prof. Dr.-Ing. Ina Schaefer)
Zentrum für Angewandte Kulturwissenschaft und Studium Generale (ZAK) (Ed.)
2023. doi:10.5445/IR/1000159235
Methods, approaches and applications in software-driven manufacturing
Vogel-Heuser, B.; Kleinert, T.; Schaefer, I.
2023. at - Automatisierungstechnik, 71 (5), 327–329. doi:10.1515/auto-2023-0033
A model-based mutation framework for IEC61131-3 manufacturing systems [Modellbasiertes Mutation-Framework für IEC61131-3 Fertigungssysteme]
Rosiak, K.; Linsbauer, L.; Vogel-Heuser, B.; Schaefer, I.
2023. at - Automatisierungstechnik, 71 (5), 380–390. doi:10.1515/auto-2022-0125
Can Quantum Computing Improve Uniform Random Sampling of Large Configuration Spaces?
Ammermann, J.; Bittner, T.; Eichhorn, D.; Schaefer, I.; Seidl, C.
2023. 2023 IEEE/ACM 4th International Workshop on Quantum Software Engineering (Q-SE), 34–41, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/q-se59154.2023.00012
Systems and software product lines of the future
ter Beek, M. H.; Schaefer, I.
2023. Journal of Systems and Software, 199, Art.-Nr.: 111622. doi:10.1016/j.jss.2023.111622
Bewertung von Fahrerassistenzsystemen im Umfeld des szenariobasierten Testens. PhD dissertation
King, C.
2023, April 13. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000157665
Correctness-by-Construction: An Overview of the CorC Ecosystem
Bordis, T.; Runge, T.; Kittelmann, A.; Schaefer, I.
2023. Ada User Journal, 44 (1), 59 – 62
Coverage-Driven Test Automation for Highly-Configurable Railway Systems
Eichhorn, D.; Pett, T.; Przigoda, N.; Kindsvater, J.; Seidl, C.; Schaefer, I.
2023. VaMoS ’23: Proceedings of the 17th International Working Conference on Variability Modelling of Software-Intensive, 23–30, Association for Computing Machinery (ACM). doi:10.1145/3571788.3571794
Providing Quantum Readiness: The Vision of the ProvideQ Toolbox
Eichhorn, D.; Schweikart, M.; Poser, N.; Osborne, T.; Schaefer, I.
2023. INFORMATIK 2023 - Designing Futures: Zukünfte gestalten, 1131 – 1135, Gesellschaft für Informatik (GI). doi:10.18420/inf2023_125
Correctness-by-Construction for Correct and Secure Software Systems. PhD dissertation
Runge, T.
2023. Technische Universität Braunschweig. doi:10.24355/dbbs.084-202306071046-0
A Query Language for Software Architecture Information
Ammermann, J.; Jordan, S.; Linsbauer, L.; Schaefer, I.
2023. Software Architecture : 17th European Conference, ECSA 2023, Istanbul, Turkey, 18th – 22nd September 2023, 337 – 345, Springer Nature Switzerland. doi:10.1007/978-3-031-42592-9_23
Automated Integration of Heteregeneous Architecture Information into a Unified Model
Jordan, S.; König, C.; Linsbauer, L.; Schaefer, I.
2023. Software Architecture – 17th European Conference, ECSA 2023, Istanbul, Turkey, September 18–22, 2023, Proceedings. Ed.: B. Tekinerdogan, 83 – 99, Springer Nature Switzerland. doi:10.1007/978-3-031-42592-9_6
Flexible Correct-by-Construction Programming
Runge, T.; Bordis, T.; Potanin, A.; Thüm, T.; Schaefer, I.
2023. Logical Methods in Computer Science, Volume 19, Issue 2 (2), 16:1 – 16:36. doi:10.46298/lmcs-19(2:16)2023
VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-Construction
Bordis, T.; Kodetzki, M.; Runge, T.; Schaefer, I.
2023. Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops – AI4EA, F-IDE, CoSim-CPS, CIFMA, Berlin, Germany, September 26–30, 2022, Revised Selected Papers. Ed.: P. Masci, 156–163, Springer International Publishing. doi:10.1007/978-3-031-26236-4_13
Model-Based Fault Classification for Automotive Software
Becker, M.; Meyer, R.; Runge, T.; Schaefer, I.; van der Wall, S.; Wolff, S.
2022. arxiv. doi:10.48550/arXiv.2208.14290
Consistent View-Based Management of Variability in Space and Time. PhD dissertation
Ananieva, S.
2022, July 26. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000148819
Family-Based and Product-Based Development of Correct-by-Construction Software Product Lines
Bordis, T.; Runge, T.; Schultz, D.; Schaefer, I.
2022. Journal of Computer Languages, 70, Art.-Nr.: 101119. doi:10.1016/j.cola.2022.101119
Verification Strategies for Feature-Oriented Software Product Lines
Kuiter, E.; Knüppel, A.; Bordis, T.; Runge, T.; Schaefer, I.
2022. Proceedings of the 16th International Working Conference on Variability Modelling of Software-Intensive Systems. Ed.: P. Arcaini, 1–9, Association for Computing Machinery (ACM). doi:10.1145/3510466.3511272
Quality-Aware Learning to Prioritize Test Cases. PhD dissertation
Omri, S.
2022, February 18. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000143079/v2
Model-Based Fault Classification for Automotive Software
Becker, M.; Meyer, R.; Runge, T.; Schaefer, I.; van der Wall, S.; Wolff, S.
2022. Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings. Ed.: I. Sergey, 110–131, Springer Nature Switzerland. doi:10.1007/978-3-031-21037-2_6
Runtime Verification of Correct-by-Construction Driving Maneuvers
Kittelmann, A.; Runge, T.; Bordis, T.; Schaefer, I.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. Ed.: T. Margaria, 242–263, Springer International Publishing. doi:10.1007/978-3-031-19849-6_15
X-by-Construction Meets Runtime Verification
ter Beek, M. H.; Cleophas, L.; Leucker, M.; Schaefer, I.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. Ed.: T. Margaria, 141–148, Springer International Publishing. doi:10.1007/978-3-031-19849-6_9
Immutability and Encapsulation for Sound OO Information Flow Control
Runge, T.; Servetto, M.; Potanin, A.; Schaefer, I.
2022. ACM Transactions on Programming Languages and Systems, 45 (1), Art.Nr. 3. doi:10.1145/3573270
Quantifying the variability mismatch between problem and solution space
Hentze, M.; Sundermann, C.; Thüm, T.; Schaefer, I.
2022. Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, 322–333, Association for Computing Machinery (ACM). doi:10.1145/3550355.3552411
Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY
Bordis, T.; Cleophas, L.; Kittelmann, A.; Runge, T.; Schaefer, I.; Watson, B. W.
2022. The Logic of Software. A Tasting Menu of Formal Methods – Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday. Ed.: W. Ahrendt, 80–104, Springer International Publishing. doi:10.1007/978-3-031-08166-8_5
A Specification Logic for Programs in the Probabilistic Guarded Command Language
Pardo, R.; Johnsen, E. B.; Schaefer, I.; Wąsowski, A.
2022. Theoretical Aspects of Computing – ICTAC 2022 – 19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022, Proceedings. Ed.: H. Seidl, 369–387, Springer International Publishing. doi:10.1007/978-3-031-17715-6_24
Information Flow Control-by-Construction for an Object-Oriented Language
Runge, T.; Kittelmann, A.; Servetto, M.; Potanin, A.; Schaefer, I.
2022. Software Engineering and Formal Methods – 20th International Conference, SEFM 2022, Berlin, Germany, September 26–30, 2022, Proceedings. Ed.: B.-H. Schlingloff, 209–226, Springer International Publishing. doi:10.1007/978-3-031-17108-6_13
AutoArx: Digital Twins of Living Architectures
Jordan, S.; Linsbauer, L.; Schaefer, I.
2022. Software Architecture – 16th European Conference, ECSA 2022, Prague, Czech Republic, September 19–23, 2022, Proceedings. Ed.: I. Gerostathopoulos, 205–212, Springer International Publishing. doi:10.1007/978-3-031-16697-6_15
Derivation of subset product lines in FeatureIDE
Linsbauer, L.; Westphal, P.; Bittner, P. M.; Krieter, S.; Thüm, T.; Schaefer, I.
2022. Proceedings of the 26th ACM International Systems and Software Product Line Conference - Volume B, 38–41, Association for Computing Machinery (ACM). doi:10.1145/3503229.3547033
Synchronizing software variants: A two-dimensional approach
König, C.; Rosiak, K.; Linsbauer, L.; Schaefer, I.
2022. Proceedings of the 26th ACM International Systems and Software Product Line Conference (SPLC ’22), Graz, A, 12.-16. September 2022. Ed.: A. Felfernig. Vol. B, 82–89, Association for Computing Machinery (ACM). doi:10.1145/3503229.3547053
Traits: Correctness-by-Construction for Free
Runge, T.; Potanin, A.; Thüm, T.; Schaefer, I.
2022. Formal Techniques for Distributed Objects, Components, and Systems – 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13–17, 2022, Proceedings. Ed.: M. Mousavi, 131–150, Springer International Publishing. doi:10.1007/978-3-031-08679-3_9
Tutorial: The Correctness-by-Construction Approach to Programming Using CorC
Schaefer, I.; Runge, T.; Cleophas, L.; Watson, B. W.
2021. 2021 IEEE Secure Development Conference (SecDev), 1–2, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/SecDev51306.2021.00012
Teaching Correctness-by-Construction and Post-hoc Verification – The Online Experience
Runge, T.; Bordis, T.; Thüm, T.; Schaefer, I.
2021. Formal Methods Teaching: 4th International Workshop and Tutorial, FMTea 2021, Virtual Event, November 21, 2021, Proceedings. Ed.: J. Ferreira, 101–116, Springer International Publishing. doi:10.1007/978-3-030-91550-6_8
Software Engineering 2021 : Fachtagung vom 22.-26. Februar 2021 Braunschweig/virtuell
Koziolek, A.; Schaefer, I.; Seidl, C. (Eds.)
2021. Gesellschaft für Informatik (GI)
Component-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures
Gerking, C.; Schubert, D.
2021. A. Koziolek, I. Schaefer & C. Seidl (Eds.), Software Engineering 2021 : Fachtagung 22.-26. Februar 2020 Braunschweig/Virtuell / Anne Koziolek, Ina Schaefer, Christoph Seidl, 43–44, Gesellschaft für Informatik (GI). doi:10.18420/SE2021_10
Proceedings of the Workshops of the Software Engineering Conference 2019, Stuttgart, Germany, February 19, 2019
Krusche, S.; Schneider, K.; Kuhrmann, M.; Heinrich, R.; Jung, R.; Konersmann, M.; Schmieders, E.; Helke, S.; Schaefer, I.; Vogelsang, A.; Annighöfer, B.; Schweiger, A.; Reich, M.; Van Hoorn, A. (Eds.)
2019. RWTH Aachen
Supporting the Development of Interdisciplinary Product Lines in the Manufacturing Domain
Kowal, M.; Ananieva, S.; Thüm, T.; Schaefer, I.
2017. IFAC-PapersOnLine, 50 (1), 4336–4341. doi:10.1016/j.ifacol.2017.08.870
Implicit Constraints in Partial Feature Models
Ananieva, S.; Kowal, M.; Thüm, T.; Schaefer, I.
2016. Proceedings of the 7th International Workshop on Feature-Oriented Software Development, 18–27, Association for Computing Machinery (ACM). doi:10.1145/3001867.3001870
Selected Challenges of Software Evolution for Automated Production Systems
Vogel-Heuser, B.; Feldmann, S.; Folmer, J.; Kowal, M.; Schaefer, I.; Ladiges, J.; Fay, A.; Haubeck, C.; Lamersdorf, W.; Lity, S.; Kehrer, T.; Tichy, M.; Getir, S.; Ulbrich, M.; Klebanov, V.; Beckert, B.
2015. 2015 IEEE 13th International Conference on Industrial Informatics (INDIN 2015) : Cambridge, United Kingdom, 22 - 24 July 2015, 314–321, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN.2015.7281753
Verification of Software Product Lines with Delta-Oriented Slicing
Bruns, D.; Klebanov, V.; Schaefer, I.
2011. Formal Verification of Object-Oriented Software. International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010. Ed.: B. Beckert, 61–75, Berlin
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse
Bruns, D.; Klebanov, V.; Schaefer, I.
2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Ed.: B. Beckert, 345–358, Karlsruher Institut für Technologie (KIT)