• Welcome
    You've reached the homepage of Christoph Haase.
    More Infos
    Christoph Haase
  • In the News
    Our LICS'15 paper on the complexity of reachability in vector addition systems with states in dimension two has been featured in the automata column of the 7th ACM SIGLOG newsletter.
    Download here.
    Left content image
  • New Paper
    Our paper "Tightening the Complexity of Equivalence Problems for Commutative Grammars" has been accepted to STACS'16.
    Download the paper
    Left content image

About Me

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.

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.

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)

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, Leibniz-Zentrum für Informatik, 2016. To appear. (PDF)
  • 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, Leibniz-Zentrum für Informatik, 2016. To appear. (PDF)
  • 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)

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

  • 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 encoded 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. The source code will be available soon.

Teaching

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

List of Courses Taught in Reverse-Chronological Order

haase@lsv.ens-cachan.fr

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

+33 147 407 568