Marko Kleine Büning

  • Institut für Theoretische Informatik

    Am Fasanengarten 5

    76131 Karlsruhe


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)