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

Programming Principles, Logic and Verification

Department of Computer Science

University College London

Carsten Fuhs

University College London Department of Computer Science Gower Street London WC1E 6BT United Kingdom E-Mail: c.fuhs@cs.ucl.ac.uk Phone: +44 20 7679 1300 Fax: +44 20 7387 1397 Room: 5.07, MPEB

Selected Activities

• Co-Organizer of the Workshop on Programming Languages and Industry at ETAPS 2015, London, UK, April 2015
• Organizer of the PPLV group's Research Seminar at UCL, since October 2014
• PC-Chair and Organizer of the 14th International Workshop on Termination (WST 2014), Vienna, Austria, July 2014
• PC-Member of the 2nd International Workshop on Haskell and Rewriting Techniques (HART 2014), Gothenburg, Sweden, September 2014
• PC-Member of the 14th/24th International Joint Workshop on Implementation of Constraint and Logic Programming Systems and Logic-based Methods in Programming Environments (CICLOPS-WLPE 2014), Vienna, Austria, July 2014
• PC-Member of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Kanazawa, Japan, June 2014
• PC-Member of the 13th International Workshop on Termination (WST 2013), Bertinoro, Italy, August 2013
• PC-Member of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012), Leuven, Belgium, September 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, from December 2008 to December 2011

Research

I am a research associate (postdoc) in the Programming Principles, Logic and Verification Group in the Department of Computer Science of University College London. Previously, I was a post-doctoral research assistant in the School of EECS at Queen Mary University of London. Earlier, I worked as a research and teaching assistant and PhD student under the supervision of Jürgen Giesl at the Research Group Computer Science 2 of RWTH Aachen University.

• Automated Termination and Complexity Analysis (development of the AProVE tool)
• Verification
• Separation Logic
• Term Rewriting
• 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, RWTH Aachen, and Dept. of Computer Science, University College London)

• Lecture Compilers (Second Term, Jan - Mar 2015)
• Lecture Compilers (Second Term, Jan - Mar 2013)
• 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)

Selected Publications

PhD Thesis

• C. Fuhs
  SAT Encodings: From Constraint-Based Termination Analysis to Circuit Synthesis
  Defended on 21 December 2011, published in 2012. Available as Technical Report AIB-2011-17, RWTH Aachen University, Germany.

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

• B. Cook, C. Fuhs, K. Nimkar, and P. O'Hearn
  Disproving Termination with Overapproximation
  In Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD '14), Lausanne, Switzerland, pages 67 - 74, 2014.
  
• T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp
  Proving Termination and Memory Safety for Programs with Pointer Arithmetic
  In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 208 - 223, 2014. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2014-05, RWTH Aachen, Germany.
  
• 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
  
• C. Fuhs and C. Kop
  First-Order Formative Rules
  In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA '14), Vienna, Austria, Lecture Notes in Computer Science (ARCoSS) 8560, pages 240 - 256, 2014. © Springer-Verlag
  
• J. Brotherston, C. Fuhs, N. Gorogiannis, and J. A. Navarro Pérez
  A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates
  In Proceedings of the Joint 23rd EACSL Annual Conference on Computer Science Logic and 29th ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS '14), Vienna, Austria, pages 25:1 - 25:10, 2014. © The Authors
  
• M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and 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 8413, pages 140 - 155, 2014. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2013-12, RWTH Aachen, Germany.
• H.-Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O'Hearn
  Proving Nontermination via Safety
  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 8413, pages 156 - 171, 2014. © Springer-Verlag
  Extended version appeared as Technical Report RN/13/23, University College London, United Kingdom.
• 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.
• J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs
  Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
  In Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12), Leuven, Belgium, pages 1 - 12, 2012. © ACM Press.
  Extended version appeared as Technical Report AIB-2012-12, RWTH Aachen, Germany.
• C. Fuhs and C. Kop
  Polynomial Interpretations for Higher-Order Rewriting
  In Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12), Nagoya, Japan, LIPIcs Leibniz International Proceedings in Informatics 15, pages 176 - 192, 2012. Dagstuhl Publishing
  
• 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 7225, pages 237 - 252, 2012. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-08, RWTH Aachen, Germany.
  
• 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
  
• 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 (fingerprint A8232351)