I am a post-doctoral researcher at the Laboratoire Spécification et Vérification at ENS Cachan working in the theory and practice of the formal verification of systems. I hold a DPhil (Ph.D.) in Computer Science from the University of Oxford, UK.

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.

- 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 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)
- C. Haase, S. Schmitz and Ph. Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science 10(4:4), 2014. (PDF | Publisher)

- M. Blondin, A. Finkel, C. Haase and S. Haddad. Approaching the Coverability Problem Continuously. In TACAS'16, LNCS. Springer, 2016. (PDF)
- C. Haase and P. Hofman. Tightening the Complexity of Equivalence Problems for Commutative Grammars. In STACS'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2016. To appear. (PDF)
- 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. 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)

- Christoph Haase, Stefan Kiefer and Markus Lohrey. Efficient Quantile Computation in Markov Chains via Counting Problems for Parikh Images, 2016. (PDF)
- Dmitry Chistikov, Christoph Haase and Simon Halfon. Context-Free Commutative Grammars with Integer Counters and Resets. Invited paper for the Special Issue of Theoretical Computer Science devoted to Selected Best Papers presented at the Reachability Problems workshop 2014. (PDF)

Here are some of my professional activities.

- ACM Transactions on Computational Logic
- Acta Informatica
- Computability - The Journal of the Association CiE
- Journal of the ACM
- Logical Methods in Computer Science
- Theoretical Computer Science

- 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)
- Logic in Computer Science (LICS)
- 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
- 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
- Markus Lohrey
- Carsten Lutz
- Pierre McKenzie
- Joel Ouaknine
- Matthew J. Parkinson
- Sylvain Schmitz
- Philippe Schnoebelen
- James Worrell

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

Laboratoire Spécification et Vérification, CNRS & ENS Cachan, 61 avenue du President Wilson, 94235 Cachan Cedex, France

© Copyright Christoph Haase 2016.