I'm a Researcher at Microsoft Research in the Programming Principles and Tools group in Cambridge.
My research focuses on automatically proving (mostly temporal) program properties, such as termination, complexity bounds or general CTL properties. My main interest is in proving these properties (or weaker versions) for large real-world programs, and thus I am mostly interested in issues of scale. Recently, I have been investigating the use of machine learning techniques in program analysis, e.g., to predict likely candidates for program or class invariants based on a few sample program runs. I am also very much interested in applying this work to problems from related areas, such as computational biology.
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. There, I focused on heap abstractions in the analysis of object-oriented programs, and details can be found on my old website.
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).
- Verification of CTL properties with first-order quantification is implemented in CTLFO (cf. evaluation).
- Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl, Lower Runtime Bounds for Integer Programs, in Proceedings of IJCAR'16, Springer, June 2016.
- Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel, Gated Graph Sequence Neural Networks, in Proceedings of ICLR'16, arXiv, May 2016.
- Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow, and He Zhu, Learning to Verify the Heap, no. MSR-TR-2016-17, April 2016.
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl, Analyzing Runtime and Size Complexity of Integer Programs, in TOPLAS, ACM – Association for Computing Machinery, April 2016.
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman, T2 : Temporal Property Verification, in Proceedings of TACAS'16, Springer, January 2016.
- Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, and Albert Rubio, Compositional Safety Verification with Max-SMT, in Proceedings of FMCAD'15, IEEE – Institute of Electrical and Electronics Engineers, September 2015.
- Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko, CTL+FO Verification as Constraint Solving, in Symposium on Model Checking of Software (SPIN), ACM, July 2014.
- Marc Brockschmidt and Andrey Rybalchenko, TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures, June 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.
- 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.