About Me

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.

Biography

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

Full-time researcher (chercheur status) in the Labex DigiCosme project VERICONISS.
Full-time researcher (chercheur status) in the ANR project ReacHard.
Six months post-doctoral research fellowship as part of an EPSRC PhD+ award.
Doctoral studies in Computer Science at the Department of Computer Science of the University of Oxford under the supervision of Joel Ouaknine. My thesis "On the Complexity of Model Checking Counter Automata" investigated algorithms for the formal verification of infinite-state systems and could solve numerous long-standing open problems in the field.
Research internship in the programming principles and tools group supervised by Byron Cook and Samin Ishtiaq. I developed and implemented graph-based algorithms for the verification of heap-manipulating programs in F#.
Combined undergraduate and graduate studies in Computer Science at the Department of Computer Science of TU Dresden, Germany, graduated with distinction and overall grade 1,2. I specialized in the theory of programming and neuro informatics. My thesis "Complexity of Subsumption in Extensions of EL" investigated polynomial-time algorithms for description logics, a knowledge representation formalism, and was supervised by Carsten Lutz.

Research Interests

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

My research is mainly focused on model-checking algorithms for concurrent infinite-state systems. I develop efficient automated reasoning procedures and model-checking algorithms for mathematical models of concurrent infinite-state systems such as counter automata, timed automata and Petri nets. Moreover, I study temporal logics used as specification languages such as CTL, LTL or MTL.
I investigate algorithms that can be used in order derive quantitative properties of systems such as timing or stochastic behavior. In particular, I have worked on algorithms for analyzing generalizations of Markov chains and Markov Decision Processes.
The main focus of my research has been on efficient decision procedures for logics used in software verification, and in particular on separation logic. The latter is a logic that is used in order to verify heap-manipulating programs.
I have worked on the computational complexity of Presburger arithmetic, an arithmetic theory that is frequently used in formal verification in order to reason about quantitative properties of systems.
I worked on automated reasoning procedures and machine learning algorithms for description logics, a knowledge representation formalism that is the basis of the Ontology Web Language (OWL).

Research Highlights

Here is a selection of some of my favorite work.

Presburger Arithmetic

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.

The Coverability Problem

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.

Separation Logic

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.

Publications

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.

Journal Publications

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

Peer-Reviewed Conference Publications

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

Book Chapters

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

Theses

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

Unpublished Manuscripts

  • M. Blondin, A. Finkel, C. Haase and S. Haddad. The Logical View on Continuous Petri Nets. Invited submission to the special issue of selected TACAS'16 papers to be published in ACM Transactions on Computational Logic (TOCL), 2016. (PDF)
  • C. Haase, S. Kiefer and M. Lohrey. Efficient Quantile Computation in Markov Chains via Counting Problems for Parikh Images, 2016. (PDF)

Tools

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

ELTL is a Java-implementation of a refinement operator for the description logic EL that can be used inside reinforcement learning frameworks and which has been integrated in the DL-learner platform, the standard platform for learning in description logics. The refinement-operator is described in our ILP'09 paper.
SeLoger is a reasoner implemented in F# and developed during an internship at Microsoft Research Cambridge that decides entailment between formulas in the fragment of separation logic with pointers and linked lists. This entailment problem is one of the fundamental decision problems needed in a separation-logic based verification framework of heap-manipulating programs. Using the graph-based approach developed in our CONCUR'11 paper, this proof-of-concept implementation outperforms all existing reasoners by several orders of magnitude on standard benchmarks from the literature. The tool is described in our CAV'13 paper; its source code is proprietary property of Microsoft Research Ltd.
QCover is a Python implementation of a decision procedure for the Petri net coverability problem that is based on applying reachability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. It is described in our TACAS'16 paper. The heart of the approach is a sophisticated encoding of reachability in continuous Petri nets into SMT which then enables QCover to use the SMT-solver Z3 in order to decide such reachability problems. Download QCover on GitHub.

Teaching

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

List of Courses Taught in Reverse-Chronological Order

christoph.haase@cs.ox.ac.uk

Department of Computer Science
University of Oxford
Wolfson Building, Room 417
Parks Rd
Oxford
OX1 3QD
United Kingdom

-
+44 1865 610669