I'm a Postdoc researcher at Microsoft Research in the Programming Principles and Tools group in Cambridge.
My research focuses on proving (mostly temporal) program properties, such as termination, complexity bounds or general CTL properties. Some of my work is implemented in T2, successor to the original TERMINATOR project. I am also very much interested in applying this work to problems from related areas.
I obtained my PhD at RWTH Aachen under the supervision of Jürgen Giesl, where I worked on termination and complexity analysis of (Java) programs in the AProVE system. There, I focussed on heap abstractions in the analysis object-oriented programs.
- Marc Brockschmidt and Andrey Rybalchenko, TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures, June 2014
- Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko, CTL+FO Verification as Constraint Solving, in SPIN, ACM, 2014
- Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, and Peter Schneider-Kamp, Proving Termination and Memory Safety for Programs with Pointer Arithmetic, in IJCAR, Springer, 2014
- Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Steffi Swiderski, and René Thiemann, Proving Termination of Programs Automatically with AProVE, in IJCAR, Springer, 2014
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Juergen Giesl, Alternating Runtime and Size Complexity Analysis of Integer Programs, in TACAS, 2014
- Marc Brockschmidt, Byron Cook, and Carsten Fuhs, Better termination proving through cooperation, in CAV, Springer, 2013
- Marc Brockschmidt, Richard Musiol, Carsten Otto, and Juergen Giesl, Automated Termination Proofs for Java Bytecode with Cyclic Data, in CAV, 2012
- Marc Brockschmidt, Thomas Stroeder, Carsten Otto, and Juergen Giesl, Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode, in FoVeOOS, 2011
- Marc Brockschmidt, Carsten Otto, and Juergen Giesl, Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting, in RTA, 2011
- Marc Brockschmidt, Carsten Otto, Christian von Essen, and Juergen Giesl, Termination Graphs for Java Bytecode, in Verification, Induction, Termination Analysis, 2010