Lehr- und Forschungsgebiet Informatik 2

Department of Computer Science

Research

I now am a post-doc researcher at Microsoft Research, and my new page is here.

I was a research assistant and PhD student at Lehr- und Forschungsgebiet Informatik 2, working on automated termination analysis of and based on term rewriting. More specifically, I worked termination analysis of heap-manipulating imperative programs with a focus on Java Bytecode. The results of my work are implemented in AProVE and T2.

• Vorlesung Formale Systeme, Automaten, Prozesse (SS 13)
• Seminar Satisfiability Checking (SS 13)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 13)
  
  
• Vorlesung Programmierung (WS 12/13)
• Seminar Verification Techniques (WS 12/13)
  
  
• Vorlesung Functional Programming (SS 12)
• Seminar Satisfiability Checking (SS 12)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 12)
  
  
• Vorlesung Programmierung (WS 11/12)
• Seminar Automated Termination Analysis (WS 11/12)
• Seminar Satisfiability Checking (WS 11/12)
  
  
• Vorlesung Term Rewriting Systems (SS 11)
• Seminar Advanced Topics in Term Rewriting (SS 11)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 11)
  
  
• Vorlesung Programmierung (WS 10/11)
• Seminar Verification Techniques (WS 10/11)
• Seminar Satisfiability Checking (WS 10/11)
  
  
• Vorlesung Formale Systeme, Automaten, Prozesse (SS 10)
• Seminar Automated Termination Analysis (SS 10)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 10)

• April 2014, Grenoble (TACAS 2014): Alternating Runtime and Size Complexity Analysis of Integer Programs
  
• November 2013, Aachen (PhD defense): Termination Analysis for Imperative Programs Operating on the Heap
  
• September 2013, Koblenz (Deduktionstreffen 2013): Better termination proving through cooperation (shortest version)
  
• July 2013, St. Petersburg (CAV 2013): Better termination proving through cooperation (shorter version)
  
• May 2013, Radboud Universiteit Nijmegen (TeReSe 2013): Better termination proving through cooperation (for term rewriters)
  
• March 2013, Microsoft Research Cambridge: Proving Termination of Heap-Manipulating Java Programs
  
• November 2012, University of Oxford: Proving Termination of Heap-Manipulating Java Programs
  
• September 2012, University College London: Proving Java Termination: Reducing the Ugly to the Bad
  
• July 2012, Berkeley (CAV 2012): Automated Termination Proofs for Java Programs with Cyclic Data
  
• February 2012, Obergurgl (WST 2012): Automated Termination Proofs for Java Bytecode with Cyclic Data
  
• February 2012, Obergurgl (WST 2012): Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  
• October 2011, Karlsruhe Institute of Technology: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  
• October 2011, Turin (FoVeOOS 2011): Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  
• May 2011, Novi Sad (RTA 2011): Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
  

• M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, J. Giesl
  Alternating Runtime and Size Complexity Analysis of Integer Programs
  In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '14), Grenoble, France, Lecture Notes in Computer Science, 2014. To appear. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2013-12, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  
  
• M. Brockschmidt, B. Cook, and C. Fuhs
  Better termination proving through cooperation
  In Proceedings of the 25th International Conference on Computer Aided Verification (CAV '13), St. Petersburg, Russia, Lecture Notes in Computer Science 8044, pages 413 - 429, 2013. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2013-06, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  
  
• M. Brockschmidt, R. Musiol, C. Otto, and J. Giesl
  Automated Termination Proofs for Java Bytecode with Cyclic Data
  In Proceedings of the 24th International Conference on Computer Aided Verification (CAV '12), Berkeley, CA, USA, Lecture Notes in Computer Science 7358, pages 105-122, 2012. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2012-06, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  
  
• M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
  Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  In Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in Computer Science 7421, pages 123-141, 2012. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-19, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  Slides for the presentation at FoVeOOS '11 (won best paper and presentation award)
  
  
• M. Brockschmidt, C. Otto, and J. Giesl
  Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
  In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia, LIPIcs Leibniz International Proceedings in Informatics 10, pages 155-170, 2011.
  Extended version including all proofs appeared as Technical Report AIB-2011-02, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  
  
• M. Brockschmidt, C. Otto, C. von Essen, and J. Giesl
  Termination Graphs for Java Bytecode
  In Verification, Induction, Termination Analysis, Lecture Notes in Artificial Intelligence 6463, pages 17-37, 2010. ©Springer-Verlag
  Extended version including all proofs appeared as Technical Report AIB-2010-15, RWTH Aachen, Germany.
  
  
• C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
  Automated Termination Analysis of Java Bytecode by Term Rewriting
  In Proceedings of the 21th International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010.
  Extended version appeared as Technical Report AIB-2010-08, RWTH Aachen, Germany.
  An experimental evaluation of the presented techniques is available.
  

• My GnuPG key