I am a Departmental Lecturer at the Department of Computer Science at the University of Oxford working on the theory and practice of the formal verification of systems.

Here are some landmarks of my professional career. Click on the items for further information.

Here are some of my research interests. Click on the items for further information.

Here is a selection of some of my favorite work.

This paper, published in CSL-LICS'14, shows that Presburger arithmetic restricted to i+1 quantifier alternations is complete for the the i-th level of the weak EXP hierarchy. This problem had been open since the 1980s. In particular, this result yields generic upper bounds for equivalence problems for a various infinite-state systems.

In this paper we develop a highly efficient approach for the coverability for Petri nets that is based on a logical characterization of reachability in continuous Petri nets. The coverability problem is, for instance, central to the automated verification of concurrent programs. Published in TACAS'16.

This paper develops a polynomial-time algorithm for entailment in the fragment of separation logic with pointers and linked lists and was published in CONCUR'11. The algorithm was the first to use a graph-theoretic approach as opposed to traditional syntactic proof search. A prototype implementation later showed that the algorithm outperforms reference reasoners by orders of magnitude.

Here is a list of my publications. Whenever applicable, the PDF offered here is the long version of the respective paper. You may also wish to consult my DBLP entry and my Google scholar profile.

- M. Blondin, A. Finkel, C. Haase and S. Haddad. The Logical View on Continuous Petri Nets. Accepted for publication (subject to minor revisions) in ACM Transactions on Computational Logic (TOCL), 2017. (PDF)
- D. Chistikov, C. Haase and S. Halfon. Context-Free Commutative Grammars with Integer Counters and Resets. Accepted for publication in Theoretical Computer Science (PDF | Publisher)
- C. Haase and S. Kiefer. The Complexity of the Kth Largest Subset Problem and Related Problems. Information Processing Letters 116(2), pages 111-115, 2016. (PDF | Publisher)
- C. Haase, J. Ouaknine and J. Worrell. Relating Reachability Problems in Timed and Counter Automata. Fundamenta Informaticae 143, pages 317-338, 2016. (PDF | Publisher)
- C. Haase, S. Schmitz and Ph. Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science 10(4:4), 2014. (PDF | Publisher)

- D. Chistikov and C. Haase. On the complexity of quantified integer programming. In ICALP'17, 2017. To appear. (PDF)
- M. Blondin and C. Haase. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. In LICS'17, 2017. To appear. (PDF)
- C. Haase, S. Kiefer and M. Lohrey. Computing Quantiles in Markov Chains with Multi-Dimensional Costs. In LICS'17, 2017. To appear. (PDF)
- D. Chistikov and C. Haase. The Taming of the Semi-Linear Set. In ICALP'16, vol. 55 of LIPIcs, pages 127:1-127:13, Leibniz-Zentrum für Informatik, 2016. (PDF | Publisher)
- S. Göller, C. Haase, R. Lazic and P. Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In ICALP'16, vol. 55 of LIPIcs, pages 105:1-105:13, Leibniz-Zentrum für Informatik, 2016. (PDF | Publisher)
- M. Blondin, A. Finkel, C. Haase and S. Haddad. Approaching the Coverability Problem Continuously. In TACAS'16, LNCS 9636, pages 480-496 . Springer, 2016. (PDF | Publisher)
- C. Haase and P. Hofman. Tightening the Complexity of Equivalence Problems for Commutative Grammars. In STACS'16, vol. 47 of LIPIcs, pages 41:1-41:14. Leibniz-Zentrum für Informatik, 2016. (PDF | Publisher)
- M. Blondin, A. Finkel, S. Göller, C. Haase and P. McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-Complete. In LICS'15, pages 32-43. ACM Press, 2015. (PDF | Publisher)
- C. Haase and S. Kiefer. The Odds of Staying on Budget. In ICALP'15, LNCS 9135, pages 234-246. Springer, 2015. (PDF | Publisher)
- C. Haase and S. Halfon. Integer Vector Addition Systems with States. In RP'14, LNCS 8762, pages 112-124. Springer, 2014. (PDF | Publisher)
- C. Haase. Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy. In CSL/LICS'14. ACM Press, 2014. (PDF | Publisher)
- T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich and J. Ouaknine. Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In FoSSaCS'14, LNCS 8412, pages 411-425. Springer, 2014. (PDF | Publisher)
- A. Finkel, S. Göller and C. Haase. Reachability in Register Machines with Polynomial Updates. In MFCS'13, LNCS 8087, pages 409-420. Springer, 2013. (PDF | Publisher)
- C. Haase, S. Schmitz and Ph. Schnoebelen. The Power of Priority Channel Systems. In CONCUR'13, LNCS 8052, pages 319-333. Springer, 2013. (PDF | Publisher)
- C. Haase, S. Ishtiaq, J. Ouaknine and M. Parkinson. SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In CAV'13, LNCS 8044, pages 790-795. Springer, 2013. (PDF | Publisher)
- C. Haase, J. Ouaknine and J. Worrell. On the Relationship between Reachability Problems in Timed and Counter Automata. In RP'12, LNCS 7550, pages 54-65. Springer, 2012. (PDF | Publisher)
- S. Göller, C. Haase, J. Ouaknine and J. Worrell. Branching-Time Model Checking of Parametric One-Counter Automata. In FoSSaCS'12, LNCS 7213, pages 406-420. Springer, 2012. (PDF | Publisher)
- B. Cook, C. Haase, J. Ouaknine, M. Parkinson and J. Worrell. Tractable Reasoning in a Fragment of Separation Logic. In CONCUR'11, LNCS 6901, pages 235-249. Springer, 2011. (PDF | Publisher)
- S. Göller, C. Haase, J. Ouaknine and J. Worrell. Model Checking Succinct and Parametric One-Counter Automata. In ICALP'10, LNCS 6199, pages 575-586. Springer, 2010. (PDF | Publisher)
- C. Haase, S. Kreutzer, J. Ouaknine and J. Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR'09, LNCS 5710, pages 369-383. Springer, 2009. (PDF | Publisher)
- J. Lehmann and C. Haase. Ideal Downward Refinement in the EL Description Logic. In ILP'09, LNCS 5989, pages 73-87. Springer, 2009. (PDF | Publisher)
- C. Haase and C. Lutz. Complexity of Subsumption in the EL Family of Description Logics: Acyclic and Cyclic TBoxes. In ECAI'08, Frontiers in Artificial Intelligence and Applications 178, pages 25-29. IOS Press, 2008. (PDF | Publisher)

- C. Haase, J. Ouaknine and J. Worrell. On Process-algebraic Extensions of Metric Temporal Logic. In Reflections on the Work of C.A.R. Hoare, History of computing, chapter 13, pages 283-300. Springer, 2010. (Publisher)

- C. Haase. On the Complexity of Model Checking Counter Automata. Ph.D. Thesis, University of Oxford, United Kingdom, January 2012. (PDF)
- C. Haase. Complexity of Subsumption in Extensions of EL. Master's Thesis, TU Dresden, Germany, August 2007. (PDF)

- C. Haase, S. Kiefer and M. Lohrey. Counting Problems for Parikh Images. 2017. Submitted. (PDF)

Here are some of my professional activities.

- 9th International Workshop on Reachability Problems (PC Member, 2015)

- Federated Logic Conference (FLOC) (Workshops Deputy Chair, 2018)
- 7th Young Researchers Workshop on Concurrency Theory (YR-CONCUR) (Co-Organizer, 2017)
- 19th International Workshop on Verification of Infinite-State Systems (INFINITY) (Co-Organizer, 2017)
- INQUEST:INnovative QUErying of STreams (Website, 2012)
- Annual Workshop of the ESF Networking Programme on Games for Design and Verification 2010 (Website and registration framework, 2010)
- 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09) (Website, 2009)

- ACM Transactions on Computational Logic
- Acta Informatica
- Computability - The Journal of the Association CiE
- Information and Computation
- Journal of Computer and System Sciences
- Journal of Logic and Algebraic Methods in Programming
- Journal of the ACM
- Logical Methods in Computer Science
- Theoretical Computer Science

- ACM Symposium on Principles of Distributed Computing (PODC)
- Computer-Aided Verification (CAV)
- Concurrency Theory (CONCUR)
- Developments in Language Theory (DLT)
- Formal Modelling and Analysis of Timed Systems (FORMATS)
- Foundations of Software Science and Computation Structures (FoSSaCS)
- Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
- Reachability Problems (RP)
- International Colloquium on Automata, Languages and Programming (ICALP)
- International Computer Science Symposium in Russia (CSR)
- International Joint Conference on Automated Reasoning (IJCAR)
- Logic in Computer Science (LICS)
- Mathematical Foundations of Computer Science (MFCS)
- Symposium on Theoretical Aspects of Computer Science (STACS)
- SOFtware SEMinar (SOFSEM)

Here are some tools that I have contributed to. Click on the items for further information.

I'm very grateful for having had multiple opportunities to work with the following people.

- Timos Antonopoulos
- Michael Blondin
- Dmitry Chistikov
- Byron Cook
- Alain Finkel
- Nikos Gorogiannis
- Stefan Göller
- Serge Haddad
- Simon Halfon
- Piotrek Hofman
- Samin Ishtiaq
- Max Kanovich
- Stefan Kiefer
- Stephan Kreutzer
- Jens Lehmann
- Ranko Lazic
- Markus Lohrey
- Carsten Lutz
- Pierre McKenzie
- Joel Ouaknine
- Matthew J. Parkinson
- Sylvain Schmitz
- Philippe Schnoebelen
- Patrick Totzke
- James Worrell

Here is a list of courses that I have been involved in.

- Machine Learning (upcoming in Michaelmas 2017, Co-Lecturer)
- Logic and Proof (2017, Lecturer)
- Machine Learning (2016, Teaching Assistant)
- Operating Systems (Systèmes d'exploitation) (2014, Co-Instructor)
- Design and Analysis of Algorithms (2012, Teaching Assistant)
- Advanced Data Structures and Algorithms (2010, Teaching Assistant)
- Integer Programming (2009, Teaching Assistant)

Office hours: Tuesdays 2-3pm (during term time)

Department of Computer Science

University of Oxford

Wolfson Building, Room 417

Parks Rd

Oxford

OX1 3QD

United Kingdom

© Copyright Christoph Haase 2016-17.