糖心logo入口

Skip to main content

Dr Carsten Fuhs

Positions held:
  • Senior Lecturer, School of Computing and Mathematical Sciences
Email
  • Overview

    Overview

    Biography

    • I am a (approx. Associate Professor in the US system) at the of 糖心logo入口, University of London.
    • Before joining 糖心logo入口 in 2015, I was a research associate (postdoc) in the in the of and in the at .
    • Earlier, I worked as a research and teaching assistant and PhD student under the supervision of at the of .

    Highlights

    • My at the in September 2025 provides a good introduction into my current research focus.

    Web profiles

    Administrative responsibilities

    • Research Theme Lead for Logical Methods research theme
    • Undergraduate Admissions Lead for the School of Computing and Mathematical Sciences

    ORCID

  • Research

    Research

    Research interests

    • Automated Termination and Complexity Analysis
    • Program Equivalence
    • Verification
    • Term Rewriting
    • Constraint Solving
    • SAT Encodings
    • Separation Logic

    Research overview

    My primary mission is to provide fully automated techniques and tools that allow software developers to check whether their code has certain (un)desirable properties, for example:

    • Termination: Is the user guaranteed to get an answer from their query to the computer, regardless of the input that the user has provided?
    • Complexity bounds: How long should the user expect to wait for the answer to their query in the worst case?
    • Equivalence: We want to replace one program by another. Can we guarantee that these two programs would always give the same answer, for all queries?
    • Safety: Is it guaranteed that the program never does anything that should not happen? (And: what, exactly, do we mean by "anything that should not happen"?)

    The goal is to answer these questions with a proof that provides mathematical certainty. The price for this lofty goal is that such verification tools can never provide a definite answer for all possible programs. However, when they do give an answer, it should be guaranteed correct, and we want our verification tools to be able to give an answer for as many (reasonable) programs as possible.

    To this end, I apply techniques and tools for deduction-based automated reasoning: relevant properties of programs can be compiled into verification-friendly intermediate languages such as (constrained) term rewriting, and the verification tasks for these problems can be handled using modern constraint solvers (e.g., SAT and SMT solvers).

    Most of my research is implemented in fully automated program analysis tools such as and .

    For a full overview of my publications, please have a look at my .

    听

    Research clusters and groups

  • Supervision and teaching

    Supervision and teaching

    Supervision

    I welcome enquiries from prospective PhD students who are interested in undertaking research in any of my areas of research interest.

    Teaching

    Teaching modules

    • Programming in Java
  • Publications

    Publications

    Article

    • Baudon, T. and Fuhs, Carsten and Gonnord, L. (2024) . Fundamenta Informaticae 192 (2), pp. 121-166. ISSN 0169-2968.
    • Frohn, F. and Fuhs, Carsten (2022) . International Journal on Software Tools for Technology Transfer 24, pp. 691-715. ISSN 1433-2779.

    Book section

    • Fuhs, Carsten and Guo, L. and Kop, C. (2025) . In: Fern谩ndez, M. (ed.) Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics. Dagstuhl Publishing. pp. 20:1-20:24. ISSN 1868-8969.
    • Milovan膷evi膰, D. and Fuhs, Carsten and Bucev, M. and Kun膷ak, V. (2024) . In: Kosmatov, N. and Kov谩cs, L. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science. Springer. pp. 75-84. ISSN 0302-9743. ISBN 9783031765537.
    • Baudon, T. and Fuhs, Carsten and Gonnord, L. (2022) . In: Villanueva, A. (ed.) Logic-Based Program Synthesis and Transformation: 32nd International Symposium, LOPSTR 2022, Tbilisi, Georgia, September 21鈥23, 2022, Proceedings. Lecture Notes in Computer Science. Springer. pp. 3-23. ISBN 9783031167669.
    • Fuhs, Carsten and Giesl, J. and Middeldorp, A. and Schneider-Kamp, P. and Thiemann, R. and Zankl, H. (2007) . In: Marques-Silva, J. and Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing: SAT 2007, 10th International Conference. Lecture Notes in Computer Science. Springer. pp. 340-354. ISBN 9783540727873.
    • Schneider-Kamp, P. and Fuhs, Carsten and Thiemann, R. and Giesl, J. and Annov, E. and Codish, M. and Middeldorp, A. and Zankl, H. (2007) . In: Baader, F. and Cook, B. and Giesl, J. and Nieuwenhuis, R. (eds.) Deduction and Decision Procedures. Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik.

    External Repositories