Lehr- und Forschungsgebiet Informatik 2

Department of Computer Science

Research

I am a research assistant and PhD student at Lehr- und Forschungsgebiet Informatik 2. I am working on automated termination analysis of and based on term rewriting. More specifically, I am working on 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)

• 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, 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. To appear. ©Springer-Verlag
  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