Overview

Research interests:

• program analysis to ensure safety and security of software systems
• modular verification of realworld embedded software
• alias anlysis in the context of verification and llvm
• automatic generation of pre- and postcondition for software modules
• verification of safety properties of neural networks

Current and previous work:

• refinement of structural abstractions with automatically generated pre and postconditions
• verifying equivalence properties of neural networks with relu activation functions (published at CP'2020)
• automatic modularization of programs for verification (published at ICFEM’19)
• development of an industrialgrade software analysis tool based on bounded model checking (at QPR Technologies, a KIT spinoff company, until 12/2018, tool published at VSTTE'20)
• unified intermediate format for bounded and unbounded software model checking (master thesis, published at ICFEM’19)
• checking information flow properties with program dependency graphs (PDGs) and interactive theorem provers (student research project, published at ICFEM’18)