Teaching Experience
- Winter 2025
- Lecture: Software Engineering (Lecturer, BSc)
- Summer 2025
- Lecture: Software Verification (Lecturer, MSc)
- Summer 2025
- Training Course: System Development with Java (Lecturer, BSc)
- Summer 2024
- Training Course: System Development with Java (TA, BSc)
- Summer 2024
- Block Course: Testing (TA, MSc)
- Winter 2023
- Seminar: Bachelor Thesis on Real-World Verification of Software (TA, BSc)
- Summer 2022
- Seminar: Machine Learning in Software Engineering (TA, BSc)
- Summer 2022
- Science and Practice in Software Engineering (TA, MSc)
- Summer 2022
- Block Course: Testing (TA, MSc)
- Winter 2021
- Block Course: Semantics of Programming Languages (TA, MSc)
- Winter 2021
- Training Course: Systematic Development of a Larger Software System (TA, Staatsexamen)
- Summer 2021
- Training Course: System Development with Java (TA, BSc)
- Summer 2021
- Block Course: Testing (TA, MSc)
- Winter 2020
- Block Course: Semantics of Programming Languages (TA, MSc)
- Winter 2020
- Tutorial: Software Verification (TA, MSc)
- Winter 2020
- Seminar: Software Quality Assurance (TA, BSc)
- Winter 2020
- Block Course: Testing (TA, MSc)
- Summer 2020
- Tutorial: Theoretical Computer Science for Media Informatics (TA, BSc)
- Winter 2019
- Training Course: System Development with Java (TA, BSc)
- Summer 2019
- Block Course: Testing (TA, MSc)
- Summer 2019
- Training Course: Advanced Software Engineering (TA, MSc)
- Winter 2018
- Training Course: System Development with Java (TA, BSc)
- Summer 2018
- Training Course: Advanced Software Engineering (TA, MSc)
- Winter 2017
- Formal Specification and Verification 2 (TA, MSc)
Student Mentoring
- Bachelor's Thesis
- A Web-First Software Analysis Tool for Visualizing Class Dependencies through Force-Directed Graph Layouts
- Bachelor's Thesis
- LLM-Based Summary Simplification for Distributed Summary Synthesis
- Bachelor's Thesis
- VerViz: A Staged Orchestrator for Integrating Software Verification into DevOps Pipelines
- Bachelor's Thesis
- Automated Task Generation for the Verification of C Program
- Bachelor's Thesis
- Creating an Exchangeable Intermediate Program Representation for the Formal Software Verifier CPAchecker
- Bachelor's Thesis
- A JSON Export for Control-Flow Automata
- Master's Thesis
- Verification of Java Micro Services based on OpenAPI Specifications
- Bachelor's Thesis
- Verification of Micro Services based on Pact API Contracts
- Master's Thesis
- Verification of Java Micro Services based on OpenAPI Specifications
- Bachelor's Thesis
- A Library for Unit Verification
- Bachelor's Thesis
- Program Transformation in CPAchecker: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code
- Research Internship
- Mining a Benchmark Set for Partial Fixes in C programs
- Master's Thesis
- Concurrent Software Verification through Block-Based Task Partitioning and Continuous Summary Refinement
- Master's Thesis
- Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification
- Bachelor's Thesis
- Mutation-Based Automatic Program Repair in CPAchecker
- Bachelor's Thesis
- A code-complexity analysis on the component level on the example of CPAchecker
- Bachelor's Thesis
- Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics
- Bachelor's Thesis
- Fault Localization for Formal Verification. An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores
- Bachelor's Thesis
- Test-Based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker
- Bachelor's Thesis
- Converting Test Goals to Condition Automata
- Bachelor's Thesis
- A Language Server and IDE Plugin for CPAchecker
- Bachelor's Thesis
- Automatic Generation of Test Harnesses for Pointer-Based C Programs. Implementation of a Pointer-Tracking Analysis and Harness-Generation Engine in the Formal Verification Framework CPAchecker
- Bachelor's Thesis
- Application of Software Verification to OpenBSD Network Modules
- Bachelor's Thesis
- Hybrid Testcase Generation with CPAchecker
- Bachelor's Thesis
- A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker
Committee Membership
- 2026
- Industry Chair of ASE 2026 (41st IEEE/ACM International Conference on Automated Software Engineering)
- 2026
- Member Organization Committee of SV-COMP 2026 (15th International Competition on Software Verification)
- 2025
- Member Organization Committee of SV-COMP 2025 (14th International Competition on Software Verification)
- 2025
- Member Artifact Evaluation of SPIN 2025 (31st International Symposium on Model Checking Software)
- 2025
- Committee Member of Test-Comp 2025 (7th International Competition on Software Testing)
- 2024
- Committee Member of Test-Comp 2024 (6th International Competition on Software Testing)
- 2023
- Committee Member of Test-Comp 2023 (5th International Competition on Software Testing)
- 2022
- Artifact-Evaluation Committee Member of CAV 2022 (34th International Conference on Computer Aided Verification)
- 2022
- Committee Member of Test-Comp 2022 (4th International Competition on Software Testing)
- 2021
- Organizer of CPA 2021 (6th International Workshop on CPAchecker)
- 2021
- Artifact-Evaluation Committee Member of VMCAI 2021 (22nd International Conference on Verification, Model Checking, and Abstract Interpretation)
- 2021
- Committee Member of Test-Comp 2021 (3rd International Competition on Software Testing)
- 2020
- Artifact-Evaluation Committee Member of PLDI 2020 (41st ACM SIGPLAN Conference on Programming Language Design and Implementation)
- 2020
- Committee Member of Test-Comp 2020 (2nd International Competition on Software Testing)
- 2019
- Judge at ACM Student Research Competition at ASE 2019 (34th IEEE/ACM International Conference on Automated Software Engineering)
- 2019
- Artifact-Evaluation Committee Member of SOSP 2019 (27th ACM Symposium on Operating Systems Principles)
- 2019
- Artifact-Evaluation Committee Member of ATVA 2019 (17th International Symposium on Automated Technology for Verification and Analysis)
- 2019
- Committee Member of Test-Comp 2019 (1st International Competition on Software Testing)
- 2018
- Program-Committee Member of SV-COMP 2018 (7th International Competition on Software Verification)
Talks
- Meeting of the Alumni of the Software Engineering Master
- Slow Productivity (Keynote) Munich, Germany
- Intel Academic Security Conference 2025
- Configurable Program Analysis for Automated Firmware Verification Hillsboro, OR, USA
- Dagstuhl Seminar 25172
- Towards Scalable and Distributed Software Verification Schloss Dagstuhl, Germany
- SV-COMP 2025
- Benchmark Presentation: Verifying Intel TDX Module Frauenchiemsee, Germany
- CPA 2024
- Multi-Processing for Distributed Summary Synthesis Milan, Italy
- SE 2024
- Towards Cooperative Software Verification with Test Generation and Formal Verification Linz, Austria
- AVM 2023
- An Experience Report on Automated Software Verification in the Real World Prague, Czechia
- CPA 2023
- Real-World Software Verification with CPAchecker Luxembourg, Luxembourg
- FASE 2022
- TestCov: New Developments and Configuration Options Virtual, Germany
- COOP 2022
- Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR Virtual, Germany
- CPA 2021
- Program Transformations with CPAchecker Virtual, Germany
- FASE 2021
- TestCov: Robust Test Execution and Coverage Measurement Virtual, Luxembourg
- FASE 2021
- PRTest: A plain random tester Virtual, Luxembourg
- CPA 2020
- Fault Localization with CPAchecker Virtual, Germany
- SEFM 2020
- Difference Verification with Conditions Virtual, Netherlands
- Paderborn 2020
- Conditional Testing: Off-the-Shelf Combination of Test-Case Generators. Paderborn, Germany Invited Talk at University of Paderborn.
- Munich 2020
- Difference Verification with Conditions. Virtual, Germany Invited Talk at ConVeY DFG Research Training Group.
- TACAS 2019
- PRTest: A plain random tester. Prague, Czech Republic
- AVM 2019
- Conditional Testing: Off-the-Shelf Combination of Test-Case Generators. Brno, Czech Republic
- ATVA 2019
- Conditional Testing: Off-the-Shelf Combination of Test-Case Generators. Taipei, Taiwan
- ASE 2019
- TestCov: Robust Test-Suite Execution and Coverage Measurement. San Diego, USA + Poster Presentation
- TACAS 2018
- CPAchecker (SV-COMP competition contribution). Thessaloniki, Greece + Poster Presentation
- ASE 2018
- CPA-SymExec: Efficient Symbolic Execution in CPAchecker. Montpellier, France + Poster Presentation
- CPA 2018
- Incremental Slicing: CEGAR + Program Slicing. Moscow, Russia
- Brno 2017
- Symbolic Execution with CEGAR in CPAchecker. Brno, Czech Republic Invited talk at Masaryk University.
- CPA 2017
- An LLVM Frontend for CPAchecker. Paderborn, Germany
- AVM 2017
- Execution-Based Validation of Verification Results. Visegrad, Hungary
- HVC 2017
- Software Verification: Testing vs. Model Checking. A Comparative Evaluation of the State of the Art. Haifa, Israel
Awards
- 2024
- PhD thesis nominated for Ernst Denert SE-Preis
- 2017
- Best-Paper Award at 13th Haifa Verification Conference
- 2016
- PROMOS Stipend for student exchange, from DAAD and University of Passau
- 2015
- Faculty price Computer Science and Mathematics, University of Passau