Lehr- und Forschungsgebiet Informatik 2

Department of Computer Science

Dr. Carsten Otto

E-Mail: otto@informatik.rwth-aachen.de Now Software Developer at andrena objects ag.

From 2008 to 2013 I was a research assistant and PhD student at Lehr- und Forschungsgebiet Informatik 2. I was working on automated termination analysis involving term rewriting. More specifically I was working on termination analysis of imperative languages with focus on Java Bytecode. The results of my work are implemented in AProVE.

• Vorlesung Logikprogrammierung (SS 13)
• Seminar Satisfiability Checking (SS 13)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 13)
  


• Vorlesung Programmierung (WS 12/13)
• Seminar Verifikationsverfahren (WS 12/13)


• Vorlesung Formale Systeme, Automaten, Prozesse (SS 12)
• Seminar Satisfiability Checking (SS 12)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 12)


• Vorlesung Programmierung (WS 11/12)
• Seminar Automatische Terminierungsanalyse (WS 11/12)
• Seminar Satisfiability Checking (WS 11/12)


• Vorlesung Formale Systeme, Automaten, Prozesse (SS 11)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 11)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 11)


• Vorlesung Logikprogrammierung (WS 10/11)
• Seminar Verifikationsverfahren (WS 10/11)
• Seminar Satisfiability Checking (WS 10/11)


• Vorlesung Formale Systeme, Automaten, Prozesse (SS 10)
• Seminar Automatische Terminierungsanalyse (SS 10)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 10)


• Vorlesung Programmierung (WS 09/10)
• Seminar Verifikationsverfahren (WS 09/10)
• Seminar Satisfiability Checking (WS 09/10)


• Vorlesung Programmierung (WS 08/09)
• Seminar Automatische Terminierungsanalyse (WS 08/09)

PhD thesis

• C. Otto
  Java Program Analysis by Symbolic Execution
  Technical Report AIB-2013-16, RWTH Aachen, Germany.
  

Conferences

• J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
  Proving Termination of Programs Automatically with AProVE
  In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 184-191, 2014. ©Springer-Verlag
  
  
• 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.
  
  
• 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.
  
• C. Fuhs, R. Navarro-Marset, C. Otto, J. Giesl, S. Lucas, and P. Schneider-Kamp
  Search Techniques for Rational Polynomial Orders
  In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC '08), Birmingham, UK, Lecture Notes in Artificial Intelligence 5144, pages 109 - 124, 2008. ©Springer-Verlag
  

• My GnuPG key