Portrait of Marc Brockschmidt

Marc Brockschmidt

Senior Principal Research Manager

Professional Activities


My work has lead to a number of (publicly available) tools:

  • A heap shape and termination analysis for heap-manipulating programs is implemented in AProVE (cf. the evaluations for Java and LLVM programs).
  • Termination analysis for integer programs is implemented in T2, successor to the original TERMINATOR project (cf. evaluation).
  • Complexity analysis for integer programs is implemented in KoAT (cf. evaluation) and LoAT (cf. evaluation)
  • Verification of CTL properties with first-order quantification is implemented in CTLFO (cf. evaluation).


I had the pleasure of working with a bunch of bright students as interns: Yuxin ChenJack Feser, Alex Gaunt, Maria GorinovaSid Krishna, Wing Lam, Yujia LiRenjie Liao, He Zhu.