Christoph Haase

Associate Professor

University of Oxford


I am an Associate Professor based in the Automated Verification Group at the Department of Computer Science at the University of Oxford and a Fellow of St Catherine’s College. The goal of my research is to develop rigorous mathematical methods, algorithms and tools that make hard- and software systems more reliable by automatically discovering bugs or proving their absence. I was awarded an ERC Starting Grant to investigate decision procedures for arithmetic theories in 2019.

I hold a D.Phil. (Ph.D.) degree from the University of Oxford and received an EPSRC doctoral prize for the accomplishments during my doctoral studies. Prior to my current appointment, I have worked at University College London, ENS Paris-Saclay and Microsoft Research Cambridge.


  • Algorithmic Verification
  • Automated Reasoning
  • Automata Theory
  • Logic in Computer Science


  • DPhil (PhD) in Computer Science, 2012

    University of Oxford, UK

  • Diplom-Informatiker (BSc/MSc in Computer Science), 2007

    Technische Universität Dresden, Germany

  • Visiting student, 2005-06

    University of Bristol, UK


Current members

Former members

  • Jakub Różycki (2020, internship student)
  • Andrei Draghici (2020, internship student)
  • Georgina Bumpus (2019, internship student)
  • Paul-Ioan Stoienescu (2019, internship student)
  • Jonathan Tanner (2019, internship student)
  • Florent Guépin (2018, internship student)
  • Simon Halfon (2014, internship student)


ARiAT is an ERC-funded project investigating decision procedures for arithmetic theories.


Invited presentations

Programme committees

Event organisation

Recent publications

(2021). Directed Reachability for Infinite-State Systems. Tools and Algorithms for the Construction and Analysis of Systems, TACAS.


(2021). On the Expressiveness of Büchi Arithmetic. Foundations of Software Science and Computation Structures, FOSSACS.


(2020). Approaching Arithmetic Theories with Finite-State Automata. Language and Automata Theory and Applications, LATA.



Summer schools

At Oxford

At ENS Cachan (now ENS Paris-Saclay)


Prospective PhD students

If you are interested in doing research on topics related to my research interests, please do get in touch for informal enquiries! I can offer a broad variety of topics to work on, ranging from fundamental problems in the theory of computation to engineering cutting-edge tools. You are of course welcome and encouraged to propose your own topics.

For more information on applying for a D.Phil. (that’s Oxford terminology for a Ph.D.), take a look at the Department’s webpage.

Previously supervised students

Research internships

  • Jakub Różycki: On the Expressiveness of Büchi Arithmetic (2020, the results appeared in FoSSaCS)
  • Andrei Draghici: Neuro-guided SAT solving (2020)
  • Georgina Bumpus, Paul-Ioan Stoienescu, Jonathan Tanner: On the Size of Finite Rational Matrix Semigroups (2019, co-supervised with S. Kiefer, the results appeared in ICALP)
  • Florent Guépin: On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields (2018, co-supervised with J. Worrell, the results appeared in LICS)
  • Simon Halfon: Non Primitive Recursive Complexity Classes (2014, co-supervised with S. Schmitz and Ph. Schnoebelen, some results appeared in RP and TCS)

Thesis supervision

  • Alex Fung: On the Expressivene Completeness of Büchi Arithmetic (2020, 4th year MEng Mathematical Computation project)
  • Andrei Draghici: Boolean Operations on Semi-Linear Sets (2019-20, 3rd year Computer Science project)
  • Serban Slincu: Decision Procedures for Linear Arithmetic Theories (2019-20, 3rd year Computer Science project)
  • Bozhidar Vasilev: Approaching Intractable Problems with SAT and SMT (2019-20, 3rd year Computer Science project)
  • Axel Ronquist: A Lower Bound on the Complexity of Real Addition Without Order (2018-19, 4th year Computer Science and Philosophy project)
  • Michał Kreft: On the Complexity of Deciding Whether Ordering is Necessary in a Presburger Formula (2017-18, 4th year Mathematics and Computer Science project)
  • Ciprian Stirbu: Parallel Algorithms for Computing Hilbert Bases (2017-18, 3rd year Computer Science project)


  • {firstname}.{lastname}@cs.ox.ac.uk
  • Departement of Computer Science, University of Oxford, Parks Rd, Oxford, OX1 3QD, United Kingdom
  • Wolfson Building, 4th floor, Room 407