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.

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

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

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

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.

Christoph Haase, Radosław Piórkowski (2023). Universal quantification makes automatic structures hard to decide. Concurrency Theory, CONCUR.

Christoph Haase, Alessio Mansutti, Amaury Pouly (2023). On Polynomial-Time Decidability of $k$-Negations Fragments of FO Theories (Extended Abstract). Mathematical Foundations of Computer Science, MFCS.

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.

Dmitry Chistikov, Christoph Haase, Alessio Mansutti (2022). Geometric decision procedures and the VC dimension of linear arithmetic theories. Logic in Computer Science, LICS.

PDF Project DOI

Dmitry Chistikov, Christoph Haase, Alessio Mansutti (2022). Quantifier elimination for counting extensions of Presburger arithmetic. Foundations of Software Science and Computation Structures, FOSSACS.

PDF Project DOI

Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, Alessio Mansutti (2022). Higher-Order Quantified Boolean Satisfiability. Mathematical Foundations of Computer Science, MFCS.

PDF Project DOI

Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, Pierre McKenzie, Patrick Totzke (2021). The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM.

Christoph Haase, Jakub Różycki (2021). On the Expressiveness of Büchi Arithmetic. Foundations of Software Science and Computation Structures, FOSSACS.

PDF Project DOI

Christoph Haase, Alessio Mansutti (2021). On deciding linear arithmetic constraints over $p$-adic integers for all primes. Mathematical Foundations of Computer Science, MFCS.

PDF Project DOI

Michael Blondin, Christoph Haase, Philip Offtermatt (2021). Directed Reachability for Infinite-State Systems. Tools and Algorithms for the Construction and Analysis of Systems, TACAS.

PDF Project DOI

Michael Blondin, Christoph Haase, Filip Mazowiecki, Mikhail Raskin (2021). Affine Extensions of Integer Vector Addition Systems with States. Log. Meth. Comput. Sci..

Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, Jonathan Tanner (2020). On the Size of Finite Rational Matrix Semigroups. Automata, Languages, and Programming, ICALP.

PDF Project DOI

Dmitry Chistikov, Christoph Haase (2020). On the power of ordering in linear arithmetic theories. Automata, Languages, and Programming, ICALP.

PDF Project DOI

Christoph Haase (2020). Approaching Arithmetic Theories with Finite-State Automata. Language and Automata Theory and Applications, LATA.

PDF Project DOI

Christoph Haase, Georg Zetzsche (2019). Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. Logic in Computer Science, LICS.

Florent Guépin, Christoph Haase, James Worrell (2019). On the Existential Theories of Büchi Arithmetic and Linear $p$-adic Fields. Logic in Computer Science, LICS.

Dmitry Chistikov, Christoph Haase, Simon Halfon (2018). Context-free commutative grammars with integer counters and resets. Theor. Comput. Sci..

Michael Blondin, Christoph Haase, Filip Mazowiecki (2018). Affine Extensions of Integer Vector Addition Systems with States. Concurrency Theory, CONCUR.

Christoph Haase (2018). A survival guide to Presburger arithmetic. SIGLOG News.

Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad (2017). The Logical View on Continuous Petri Nets. ACM Trans. Comput. Log..

Dmitry Chistikov, Christoph Haase (2017). On the Complexity of Quantified Integer Programming. Automata, Languages, and Programming, ICALP.

Michael Blondin, Christoph Haase (2017). Logics for continuous reachability in Petri nets and vector addition systems with states. Logic in Computer Science, LICS.

Christoph Haase, Stefan Kiefer, Markus Lohrey (2017). Counting Problems for Parikh Images. Mathematical Foundations of Computer Science, MFCS.

Christoph Haase, Stefan Kiefer, Markus Lohrey (2017). Computing quantiles in Markov chains with multi-dimensional costs. Logic in Computer Science, LICS.

Christoph Haase, Piotr Hofman (2016). Tightening the Complexity of Equivalence Problems for Commutative Grammars. Symposium on Theoretical Aspects of Computer Science, STACS.

Dmitry Chistikov, Christoph Haase (2016). The Taming of the Semi-Linear Set. Automata, Languages, and Programming, ICALP.

Christoph Haase, Stefan Kiefer (2016). The complexity of the $K$th largest subset problem and related problems. Inf. Process. Lett..

Christoph Haase, Joël Ouaknine, James Worrell (2016). Relating Reachability Problems in Timed and Counter Automata. Fundam. Inform..

Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad (2016). Approaching the Coverability Problem Continuously. Tools and Algorithms for the Construction and Analysis of Systems, TACAS.

Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke (2016). A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. Automata, Languages, and Programming, ICALP.

Christoph Haase, Stefan Kiefer (2015). The Odds of Staying on Budget. Automata, Languages, and Programming, ICALP.

Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, Pierre McKenzie (2015). Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. Logic in Computer Science, LICS.

Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen (2014). The Power of Priority Channel Systems. Log. Meth. Comput. Sci..

Christoph Haase (2014). Subclasses of Presburger arithmetic and the weak EXP hierarchy. Computer Science Logic and Logic in Computer Science, CSL-LICS.

Christoph Haase, Simon Halfon (2014). Integer Vector Addition Systems with States. Reachability Problems, RP.

Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, Joël Ouaknine (2014). Foundations for Decision Problems in Separation Logic with General Inductive Predicates. Foundations of Software Science and Computation Structures, FOSSACS.

Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen (2013). The Power of Priority Channel Systems. Concurrency Theory, CONCUR.

Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson (2013). SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. Computer Aided Verification, CAV.

Alain Finkel, Stefan Göller, Christoph Haase (2013). Reachability in Register Machines with Polynomial Updates. Mathematical Foundations of Computer Science, MFCS.

Christoph Haase, Joël Ouaknine, James Worrell (2012). On the Relationship between Reachability Problems in Timed and Counter Automata. Reachability Problems, RP.

Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell (2012). Branching-Time Model Checking of Parametric One-Counter Automata. Foundations of Software Science and Computational Structures, FOSSACS.

Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell (2011). Tractable Reasoning in a Fragment of Separation Logic. Concurrency Theory, CONCUR.

Christoph Haase, Joël Ouaknine, James Worrell (2010). On Process-Algebraic Extensions of Metric Temporal Logic. Reflections on the Work of C. A. R. Hoare..

Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell (2010). Model Checking Succinct and Parametric One-Counter Automata. Automata, Languages and Programming, ICALP.

Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell (2009). Reachability in Succinct and Parametric One-Counter Automata. Concurrency Theory, CONCUR.

Jens Lehmann, Christoph Haase (2009). Ideal Downward Refinement in the $mathcalEL$ Description Logic. Inductive Logic Programming, ILP.

Christoph Haase, Carsten Lutz (2008). Complexity of Subsumption in the $mathcalEL$ Family of Description Logics: Acyclic and Cyclic TBoxes. European Conference on Artificial Intelligence, ECAI.