Dr Carsten Fuhs

Overview

Biography

• I am a Senior Lecturer (approx. Associate Professor in the US system) at the School of Computing and Mathematical Sciences 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.

Qualifications

• PhD, RWTH Aachen University, 2012

Web profiles

• Personal web page

Administrative responsibilities

• Group Lead for Logical Methods research group
• Undergraduate Admissions Lead for the School of Computing and Mathematical Sciences

Research

Research interests

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

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 AProVE and Cora.

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

Research clusters and groups

• Group Lead, Logical Methods research group

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 (BUCI033S7)

Publications