Carsten Fuhs

Birkbeck, University of London School of Computing and Mathematical Sciences Malet Street London WC1E 7HX United Kingdom E-Mail: c.fuhs@bbk.ac.uk Phone: +44 20 3926 1278 Fax: +44 20 7631 6727 Room: MAL154 (Main Building)

Selected Activities

• Member of the Board of Trustees of the International Conference on Automated Deduction (CADE), since 2023
• Member of the Executive Committee of ACM SIGLOG, since 2023
• 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
• Co-Chair of the IFIP Working Group 1.6 on Rewriting, since 2021; member since 2020
• Chair of the Expert Committee for the Bill McCune PhD Award in Automated Reasoning 2024 (for 2023), 2024
• Lecturer at the SAT/SMT/AR Summer School 2024, Nancy, France, June 2024 (material)
• PC-Member of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2024
• PC-Member of the 17th International Symposium on Functional and Logic Programming (FLOPS 2024), Kumamoto, Japan, May 2024
• PC-Chair of the 11th International Workshop on Higher-Order Rewriting (HOR 2023), Rome, Italy, July 2023
• PC-Member of the 19th International Workshop on Termination (WST 2023), Obergurgl, Austria, August 2023
• PC-Member of the 12th International Workshop on Confluence (IWC 2023), Obergurgl, Austria, August 2023
• Member of the Expert Committee for the Bill McCune PhD Award in Automated Reasoning 2023 (for 2022), 2023
• PC-Member of the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July 2023
• PC-Member of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023), Rome, Italy, July 2023
• Lecturer at the 13th International School on Rewriting (ISR 2022), Tbilisi, Georgia, September 2022 (material)
• Lecturer at the EuroProofNet Summer School on Verification Technology, Systems & Applications 2022, Saarbrücken, Germany, September 2022 (material)
• Member of the Expert Committee for the Bill McCune PhD Award in Automated Reasoning 2022 (for 2021), 2022
• PC-Member of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Haifa, Israel, August 2022
• PC-Member of the 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP 2022), San Diego, USA, June 2022
• Lecturer at the 12th International School on Rewriting (ISR 2021), Madrid, Spain, July 2021 (material)
• Member of the Expert Committee for the Bill McCune PhD Award in Automated Reasoning 2021 (for 2019 and 2020), 2021.
• PC-Member 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
• PC-Member of the 17th International Workshop on Termination (WST 2020), Paris, France, July 2020 postponed to 2021
• Lecturer at the 12th International School on Rewriting (ISR 2020), Madrid, Spain, July 2020 postponed to July 2021
• Co-Organizer of Dagstuhl Seminar 19371 - Deduction Beyond Satisfiability, Dagstuhl, Germany, September 2019
• PC-Member of the 5th International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA 2019), Tbilisi, Georgia, November 2019
• Organizer of the 10th South of England Regional Programming Language Seminar (S-REPLS 10), London, UK, September 2018
• PC-Member of the 16th International Workshop on Termination (WST 2018), Oxford, UK, July 2018
• PC-Member of the 14th International Symposium on Functional and Logic Programming (FLOPS 2018), Nagoya, Japan, May 2018
• Co-Organizer of Dagstuhl Seminar 17371 - Deduction Beyond First-Order Logic, Dagstuhl, Germany, September 2017
• Lecturer at the 9th International School on Rewriting (ISR 2017), Eindhoven, The Netherlands, July 2017 (material)
• PC-Member 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
• Co-Organizer 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
• PC-Member of the 2nd International Workshop on Haskell and Rewriting Techniques (HART 2014), Gothenburg, Sweden, September 2014
• PC-Chair and Organizer of the 14th International Workshop on Termination (WST 2014), Vienna, Austria, July 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 senior lecturer (≈ associate professor) at the Department of Computer Science and Information Systems of Birkbeck, University of London. Before joining Birkbeck in 2015, 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.

• Automated Termination and Complexity Analysis (development of the AProVE tool)
• Program Equivalence
• 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

• Lecture Programming in Java (Term 1, Oct - Dec 2023)
• Lecture Programming in Java (Term 1, Oct - Dec 2022)
• Lecture Software and Programming II (Term 1, Oct - Dec 2021)
• 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)

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

• F. Frohn and C. Fuhs
  A Calculus for Modular Loop Acceleration and Non-Termination Proofs
  International Journal on Software Tools for Technology Transfer, 24:691-715, 2022.
  Preliminary Version
  
• 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. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
  Analyzing Program Termination and Complexity Automatically with AProVE
  Journal of Automated Reasoning, 58(1):3-31, 2017. © Springer-Verlag
  The final publication is available at Springer via the DOI 10.1007/s10817-016-9388-y.
  Preliminary Version
  
• T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, P. Schneider-Kamp, and C. Aschermann
  Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
  Journal of Automated Reasoning, 58(1):33-65, 2017. © Springer-Verlag
  The final publication is available at Springer via the DOI 10.1007/s10817-016-9389-x.
  Preliminary Version
  Extended version appeared as Technical Report AIB-2016-09, 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. 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

• T. Baudon, C. Fuhs, and L. Gonnord
  Analysing Parallel Complexity of Term Rewriting
  In Proceedings of the 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '22), Tbilisi, Georgia, Lecture Notes in Computer Science 13474, pages 3 - 23, 2022. © The Authors. Best Paper Award.
  
• 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. © Springer-Verlag.
  
• C. Fuhs and C. Kop
  A Static Higher-Order 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. Springer-Verlag.
  
• 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. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2017-05, 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 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)