You should be redirected automatically within 5 seconds. Should this fail for some reason, please manually go to my new home page.

Lehr- und Forschungsgebiet Informatik 2

Department of Computer Science

Carsten Fuhs

Lehr- und Forschungsgebiet Informatik 2 RWTH Aachen 52056 Aachen Germany E-Mail: at informatik dot rwth-aachen.de Phone: +49-241/80-21241 Fax: +49-241/80-22217 Room: 4209, Ahornstr. 55

Current Activities

• PC-Member of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012), 2012
• PC-Member of the 21st Workshop on Logic-based methods in Programming Environments (WLPE 2011), Lexington, KY, USA, July 2011
• Organizer of TeReSe meeting 2010/1, Aachen, May 2010
• Proceedings collector of Dagstuhl Seminar 09411 - Interaction versus Automation: The two Faces of Deduction, October 2009
• Editor of the Department Of Computer Science Technical Reports of RWTH Aachen University, since December 2008

Research

I am a research assistant and PhD student at Lehr- und Forschungsgebiet Informatik 2. My fields of interest include:

• Termination and Complexity Analysis (AProVE tool)
• Verification
• SAT Encodings
  • Benchmark submissions to the SAT Competition 2011:
    • AProVE 11: Benchmarks, Description
    • SLP Synthesis for AES: Benchmarks, Description
  • Benchmark submission to the SAT Competition 2009: Benchmarks, Description
  • Benchmark submission to the SAT Competition 2007: Benchmarks, Description
• SAT Solving (Contributor to SAT4J: The Java SAT Library)

Teaching Activities (Lehr- und Forschungsgebiet Informatik 2)

• Vorlesung Term Rewriting Systems (SS 11)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 11)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 11)
• Vorlesung Logic Programming (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 Functional Programming (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)
• Vorlesung Formale Systeme, Automaten, Prozesse (SS 08)
• Seminar Verifikationsverfahren (SS 08)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 08)
• Vorlesung Programmierung (WS 07/08)
• Seminar Automatische Terminierungsanalyse (WS 07/08)
• Vorlesung Formale Systeme, Automaten, Prozesse (SS 07)
• Seminar Verifikationsverfahren (SS 07)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 07)

Publications

Journals

• C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, and S. Swiderski
  Proving Termination by Dependency Pairs and Inductive Theorem Proving
  Journal of Automated Reasoning, 47(2):133-160, 2011. © Springer-Verlag
  
• M. Codish, I. Gonopolskiy, A. Ben-Amram, C. Fuhs, and J. Giesl
  SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers
  In Proceedings of the 27th International Conference on Logic Programming (ICLP '11), Lexington, KY, USA, Theory and Practice of Logic Programming, 11(4-5):503-520, 2011. © Cambridge University Press
  

Conferences

• C. Fuhs and C. Kop
  Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
  In Proceedings of the 8th International Symposium Frontiers of Combining Systems (FroCoS '11), Saarbrücken, Germany, Lecture Notes in Artificial Intelligence 6989, pages 147 - 162, 2011. © Springer-Verlag
  
• T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs
  A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
  In Proceedings of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '11), Odense, Denmark, Lecture Notes in Computer Science. To appear. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-08, RWTH Aachen, Germany.
  
• A. Krauss, C. Sternagel, R. Thiemann, C. Fuhs, and J. Giesl
  Termination of Isabelle Functions via Termination of Rewriting
  In Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP '11), Nijmegen, The Netherlands, Lecture Notes in Computer Science 6898, pages 152 - 167, 2011. © Springer-Verlag
  
• M. Codish, Y. Fekete, C. Fuhs, and P. Schneider-Kamp
  Optimal Base Encodings for Pseudo-Boolean Constraints
  In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '11), Saarbrücken, Germany, Lecture Notes in Computer Science 6605, pages 189 - 204, 2011. © Springer-Verlag
  
• M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp
  Lazy Abstraction for Size-Change Termination
  In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Yogyakarta, Indonesia, Lecture Notes in Computer Science (ARCoSS) 6397, pages 217 - 232, 2010. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2010-14, RWTH Aachen, Germany.
  
• C. Fuhs and P. Schneider-Kamp
  Synthesizing Shortest Straight-Line Programs over GF(2) using SAT
  In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT '10), Edinburgh, UK, Lecture Notes in Computer Science 6175, pages 71 - 84, 2010. © Springer-Verlag
  
• S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. Schneider-Kamp
  Termination Analysis by Dependency Pairs and Inductive Theorem Proving
  In Proceedings of the 22nd International Conference on Automated Deduction (CADE '09), Montréal, Canada, Lecture Notes in Artificial Intelligence 5663, pages 322 - 338, 2009. © Springer-Verlag
  
• C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke
  Proving Termination of Integer Term Rewriting
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasília, Brazil, Lecture Notes in Computer Science 5595, pages 32 - 47, 2009. © Springer-Verlag
  
• B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann
  Improving Context-Sensitive Dependency Pairs
  In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, Lecture Notes in Artificial Intelligence 5330, pages 636 - 651, 2008. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2008-13, RWTH Aachen, Germany.
  
• 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
  
• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  Maximal Termination
  In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 110 - 125, 2008. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2008-03, RWTH Aachen, Germany.
  
• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  SAT Solving for Termination Analysis with Polynomial Interpretations
  In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT '07), Lisbon, Portugal, Lecture Notes in Computer Science 4501, pages 340 - 354, 2007. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2007-02, RWTH Aachen, Germany.
  

Miscellaneous

• My GPG key