
Carsten Fuhs


 Birkbeck, University of London
 Department of Computer Science and Information Systems
 Malet Street
 London WC1E 7HX
 United Kingdom
EMail: carsten@dcs.bbk.ac.uk
 Phone: +44 20 7631 6598
 Fax: +44 20 7631 6727
 Room: MAL154 (Main Building)


 Publicity Chair of the International Conference on Formal Structures for Computation and Deduction (FSCD), since 2020
 Member of the Steering Committee of the International Conference on Formal Structures for Computation and Deduction (FSCD), since 2017
 Member of the IFIP Working Group 1.6 on Rewriting, since 2020
 PCMember of the 17th International Workshop on Termination (WST 2021), Pittsburgh, USA, July
2021
 Invited Speaker at the 22nd Meeting of the IFIP Working Group 1.6
on Rewriting, Paris, France, June 2020
 Lecturer at the 12th International School on Rewriting (ISR 2020),
Madrid, Spain,
July 2020 postponed to 2021
 PCMember of the 17th International Workshop on Termination (WST 2020),
Paris, France, July
2020 postponed to 2021
 CoOrganizer of Dagstuhl Seminar 19371  Deduction Beyond Satisfiability, Dagstuhl, Germany, September 2019
 Organizer of the 10th South of England Regional Programming Language Seminar (SREPLS 10), London, UK, September 2018
 PCMember of the 16th International Workshop on Termination (WST 2018), Oxford, UK, July 2018
 PCMember of the 14th International Symposium on Functional and Logic Programming (FLOPS 2018), Nagoya, Japan, May 2018
 CoOrganizer of Dagstuhl Seminar 17371  Deduction Beyond FirstOrder Logic, Dagstuhl, Germany, September 2017
 Lecturer at the 9th International School on Rewriting (ISR 2017), Eindhoven, The Netherlands, July 2017
 PCMember of the 4th International Conference on Tools and Methods of Program Analysis (TMPA 2017), Moscow, Russia, March 2017
 Invited Speaker at the 8th Danish Static Analysis Symposium (DANSAS 2016), Odense, Denmark, August 2016
 Invited Speaker at the 14th International Workshop on Satisfiability Modulo Theories (SMT 2016), Coimbra, Portugal, July 2016
 Review Editor for the Formal Methods section of Frontiers in ICT, since July 2015
 CoOrganizer of the Workshop on Programming Languages in Industry at ETAPS 2015, London, UK, April 2015
 Organizer of the PPLV group's Research Seminar at UCL, from October 2014 to June 2015
 PCMember of the 2nd International Workshop on Haskell and Rewriting Techniques (HART 2014), Gothenburg, Sweden, September 2014
 PCChair and Organizer of the 14th International Workshop on Termination (WST 2014), Vienna, Austria, July 2014
 PCMember of the 14th/24th International Joint Workshop on Implementation of Constraint and Logic Programming Systems and Logicbased Methods in Programming Environments (CICLOPSWLPE 2014), Vienna, Austria, July 2014
 PCMember of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Kanazawa, Japan, June 2014
 PCMember of the 13th International Workshop on Termination (WST 2013), Bertinoro, Italy, August 2013
 PCMember of the 22nd International Symposium on LogicBased
Program Synthesis and Transformation (LOPSTR 2012), Leuven, Belgium,
September 2012
 PCMember of the 21st Workshop on Logicbased 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
I am a lecturer (≈ assistant professor) at the
Department of Computer Science and Information Systems of
Birkbeck, University of London.
Previously, I was a research associate (postdoc) in the
Programming Principles, Logic and Verification Group
in the Department of Computer Science
of University College London
and
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.
My fields of interest include:
 Lecture Software and Programming I (Term 2, Jan  Mar 2021)
 Lecture Software and Programming II (Term 1, Oct  Dec 2020)
 Lecture Software and Programming I (Term 2, Jan  Mar 2020)
 Lecture Software and Programming II (Term 1, Sep  Dec 2019)
 Lecture Software and Programming I (Term 2, Jan  Mar 2019)
 Lecture Software and Programming II (Term 1, Oct  Dec 2018)
 Lecture Software and Programming I (Term 2, Jan  Mar 2018)
 Lecture Software and Programming II (Term 1, Oct  Dec 2017)
 Lecture Software and Programming I (Term 2, Jan  Mar 2017)
 Lecture Software and Programming II (Term 1, Oct  Dec 2016)
 Lecture Software and Programming II (Term 1, Sep  Dec 2015)
 Lecture Compilers (Term 2, Jan  Mar 2015)
 Lecture Compilers (Term 2, 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)
PhD Thesis
Journals
 C. Fuhs, C. Kop, and N. Nishida
Verifying Procedural Programs via Constrained Rewriting Induction
ACM Transactions on Computational Logic, 18(2):14, 2017.
Preliminary Version
 J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker,
P. SchneiderKamp, T. Ströder, S. Swiderski, and R. Thiemann
Analyzing Program Termination and Complexity Automatically with AProVE
Journal of Automated Reasoning, 58(1):331, 2017. ©
SpringerVerlag
The final publication is available at Springer via the
DOI 10.1007/s108170169388y.
Preliminary Version
 T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, P. SchneiderKamp, and C. Aschermann
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Journal of Automated Reasoning, 58(1):3365, 2017. ©
SpringerVerlag
The final publication is available at Springer via the
DOI 10.1007/s108170169389x.
Preliminary Version
Extended version appeared as Technical Report AIB201609, RWTH Aachen, Germany.
 M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl
Analyzing Runtime and Size Complexity of Integer Programs
ACM Transactions on Programming Languages and Systems, 38(4):13, 2016. ACM
Preliminary Version
 C. Fuhs, J. Giesl, M. Parting, P. SchneiderKamp, and S. Swiderski
Proving Termination by Dependency Pairs and Inductive Theorem Proving
Journal of Automated Reasoning, 47(2):133160, 2011. ©
SpringerVerlag
 M. Codish, I. Gonopolskiy, A. BenAmram, C. Fuhs, and J. Giesl
SATBased 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(45):503520, 2011.
© Cambridge University Press
Conferences
 C. Fuhs
Transforming Derivational Complexity of Term Rewriting to Runtime Complexity
In Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS '19),
London, United Kingdom, Lecture Notes in Artificial Intelligence 11715, pages 348  364, 2019.
© SpringerVerlag.
 C. Fuhs and C. Kop
A Static HigherOrder Dependency Pair Framework
In Proceedings of the 28th European Symposium on Programming (ESOP '19),
Prague, Czech Republic, Lecture Notes in Computer Science 11423, pages 752  782, 2019.
SpringerVerlag.
 M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl
Complexity Analysis for Term Rewriting by Integer Transition Systems
In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17),
Brasília, Brazil, Lecture Notes in Artificial Intelligence 10483, pages 132  150, 2017.
© SpringerVerlag
Extended version
appeared as Technical Report AIB201705, RWTH Aachen, Germany.
 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 ComputerAided Design (FMCAD '14),
Lausanne, Switzerland, pages 67  74, 2014.
 T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. SchneiderKamp
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.
© SpringerVerlag
Extended version
appeared as Technical Report AIB201405, RWTH Aachen, Germany.
 J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto,
M. Plücker, P. SchneiderKamp, 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.
© SpringerVerlag
 C. Fuhs and C. Kop
FirstOrder 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 (RTATLCA '14),
Vienna, Austria, Lecture Notes in Computer Science (ARCoSS) 8560,
pages 240  256, 2014.
© SpringerVerlag
 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 (CSLLICS '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.
© SpringerVerlag
Extended version appeared as
Technical Report AIB201312, 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.
© SpringerVerlag
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.
© SpringerVerlag
Extended version appeared as
Technical Report AIB201306, RWTH Aachen, Germany.
 J. Giesl, T. Ströder, P. SchneiderKamp, 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 AIB201212, RWTH Aachen, Germany.
 C. Fuhs and C. Kop
Polynomial Interpretations for HigherOrder 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. SchneiderKamp, 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
LogicBased Program Synthesis and Transformation (LOPSTR '11),
Odense, Denmark, Lecture Notes in Computer Science 7225, pages 237  252, 2012.
© SpringerVerlag
Extended version appeared as
Technical Report AIB201108, 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.
© SpringerVerlag
 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.
©
SpringerVerlag
 M. Codish, Y. Fekete, C. Fuhs, and P. SchneiderKamp
Optimal Base Encodings for PseudoBoolean 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.
© SpringerVerlag
 M. Codish, C. Fuhs, J. Giesl, and P. SchneiderKamp
Lazy Abstraction for SizeChange Termination
In Proceedings of the 17th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR17),
Yogyakarta, Indonesia, Lecture Notes in Computer Science (ARCoSS) 6397,
pages 217  232, 2010.
© SpringerVerlag
Extended version appeared as
Technical Report AIB201014, RWTH Aachen, Germany.
 C. Fuhs and P. SchneiderKamp
Synthesizing Shortest StraightLine 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.
© SpringerVerlag
 S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. SchneiderKamp
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. ©
SpringerVerlag
 C. Fuhs, J. Giesl, M. Plücker, P. SchneiderKamp, 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. ©
SpringerVerlag
 B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez,
S. Lucas, P. SchneiderKamp, and R. Thiemann
Improving ContextSensitive
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. ©
SpringerVerlag
Extended version appeared as
Technical Report AIB200813, RWTH Aachen, Germany.

C. Fuhs, R. NavarroMarset, C. Otto, J. Giesl, S. Lucas, and P. SchneiderKamp
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.
©
SpringerVerlag
 C. Fuhs, J. Giesl, A. Middeldorp, P. SchneiderKamp, 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.
©
SpringerVerlag
Extended version appeared as Technical Report AIB200803, RWTH Aachen, Germany.

C. Fuhs, J. Giesl, A. Middeldorp, P. SchneiderKamp, 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.
©
SpringerVerlag
Extended version appeared as Technical Report AIB200702, RWTH Aachen, Germany.
Carsten Fuhs 
Last modified: Mon Dec 14 15:40:04 GMT 2020
