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


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