Welcome

You’ve reached the homepage of Christoph Haase

Previous Next

News

Advanced Course at ESSLLI 2023
Post-Doc Opening -- Deadline January 2023
World Logic Day
Post-Doc Opening -- Deadline July 2022
ICALP satellite workshop 'Trends in Arithmetic Theories'
See all posts
Avatar

Christoph Haase

Associate Professor

University of Oxford

Biography

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. In 2019, I was awarded an ERC Starting Grant to investigate decision procedures for arithmetic theories. I currently serve as an Associate Editor for the Journal of Computer and System Sciences.

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.

Interests

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

Education

  • 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

Team

Current members

Research Associates

DPhil (PhD) Students

Former members

Projects

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

Events

Programme committees

Invited presentations

Event organisation

Recent publications

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, Georg Zetzsche (2024). An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. International Colloquium on Automata, Languages, and Programming, ICALP.

PDF DOI

Rémy Défossez, Christoph Haase, Alessio Mansutti, Guillermo A. Pérez (2024). Integer Programming with GCD Constraints. Symposium on Discrete Algorithms, SODA.

PDF DOI

Andrei Draghici, Christoph Haase, Andrew Ryzhikov (2024). Reachability in Fixed VASS: Expressiveness and Lower Bounds. Foundations of Software Science and Computation Structures, FoSSaCS.

PDF DOI

Andrei Draghici, Christoph Haase, Florin Manea (2024). Semënov Arithmetic, Affine VASS, and String Constraints. Symposium on Theoretical Aspects of Computer Science, STACS.

PDF DOI

Przemysław Andrzej Wałęga, Michal Zawidzki, Christoph Haase (2023). Computing All Facts Entailed By An LTL Specification. Principals of Knowledge Representation and Reasoning, KR.

PDF DOI

See all publications

Teaching

Summer schools

At Oxford

At ENS Cachan (now ENS Paris-Saclay)

Students

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

DPhil (PhD) students

Research internships/visiting students

  • Pascal Baumann (2024)
  • Aleksander Wiśniewski: Farkas’ lemma for linear Horn systems (2023)
  • Jacob Ginesin: Directed reachability for finite-state systems (2023)
  • Zahra Hadizadeh: Higher-Order Satisfiability Problems and Weak Presburger Arithmetic (2021, co-supervised with A. Mansutti, the results appeared in MFCS)
  • 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 Expressive 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)

Contact

  • {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

Legal

Image credits