| 2025 | DLT | Formal Languages and Arithmetic Theories: Recent Results and Open Problems. | Christoph Haase, Mikhail R. Starchak |
| 2025 | SETTA | MPL - A Flexible Multiprecision Library. | Jonathan Tanner, Christoph Haase |
| 2024 | FOSSACS | Reachability in Fixed VASS: Expressiveness and Lower Bounds. | Andrei Draghici, Christoph Haase, Andrew Ryzhikov |
| 2024 | ICALP | An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. | Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, Georg Zetzsche |
| 2024 | SODA | Integer Programming with GCD Constraints. | Rmy Dfossez, Christoph Haase, Alessio Mansutti, Guillermo A. Prez |
| 2024 | STACS | Semnov Arithmetic, Affine {VASS}, and String Constraints. | Andrei Draghici, Christoph Haase, Florin Manea |
| 2023 | CONCUR | Universal Quantification Makes Automatic Structures Hard to Decide. | Christoph Haase, Radoslaw Pirkowski |
| 2023 | KR | Computing All Facts Entailed By An LTL Specification. | Przemyslaw Andrzej Walega, Michal Zawidzki, Christoph Haase |
| 2023 | MFCS | On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract). | Christoph Haase, Alessio Mansutti, Amaury Pouly |
| 2022 | FOSSACS | Quantifier elimination for counting extensions of Presburger arithmetic. | Dmitry Chistikov, Christoph Haase, Alessio Mansutti |
| 2022 | LICS | Geometric decision procedures and the VC dimension of linear arithmetic theories. | Dmitry Chistikov, Christoph Haase, Alessio Mansutti |
| 2022 | MFCS | Higher-Order Quantified Boolean Satisfiability. | Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, Alessio Mansutti |
| 2021 | FOSSACS | On the Expressiveness of Bchi Arithmetic. | Christoph Haase, Jakub Rzycki |
| 2021 | MFCS | On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes. | Christoph Haase, Alessio Mansutti |
| 2021 | TACAS | Directed Reachability for Infinite-State Systems. | Michael Blondin, Christoph Haase, Philip Offtermatt |
| 2020 | ICALP | On the Size of Finite Rational Matrix Semigroups. | Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, Jonathan Tanner |
| 2020 | ICALP | On the Power of Ordering in Linear Arithmetic Theories. | Dmitry Chistikov, Christoph Haase |
| 2020 | LATA | Approaching Arithmetic Theories with Finite-State Automata. | Christoph Haase |
| 2019 | LICS | On the Existential Theories of Bchi Arithmetic and Linear p-adic Fields. | Florent Gupin, Christoph Haase, James Worrell |
| 2019 | LICS | Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. | Christoph Haase, Georg Zetzsche |
| 2018 | CONCUR | Affine Extensions of Integer Vector Addition Systems with States. | Michael Blondin, Christoph Haase, Filip Mazowiecki |
| 2017 | ICALP | On the Complexity of Quantified Integer Programming. | Dmitry Chistikov, Christoph Haase |
| 2017 | LICS | Logics for continuous reachability in Petri nets and vector addition systems with states. | Michael Blondin, Christoph Haase |
| 2017 | LICS | Computing quantiles in Markov chains with multi-dimensional costs. | Christoph Haase, Stefan Kiefer, Markus Lohrey |
| 2017 | MFCS | Counting Problems for Parikh Images. | Christoph Haase, Stefan Kiefer, Markus Lohrey |
| 2016 | ICALP | The Taming of the Semi-Linear Set. | Dmitry Chistikov, Christoph Haase |
| 2016 | ICALP | A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. | Stefan Gller, Christoph Haase, Ranko Lazic, Patrick Totzke |
| 2016 | STACS | Tightening the Complexity of Equivalence Problems for Commutative Grammars. | Christoph Haase, Piotr Hofman |
| 2016 | TACAS | Approaching the Coverability Problem Continuously. | Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad |
| 2015 | ICALP | The Odds of Staying on Budget. | Christoph Haase, Stefan Kiefer |
| 2015 | LICS | Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. | Michael Blondin, Alain Finkel, Stefan Gller, Christoph Haase, Pierre McKenzie |
| 2014 | CSL | Subclasses of presburger arithmetic and the weak EXP hierarchy. | Christoph Haase |
| 2014 | FOSSACS | Foundations for Decision Problems in Separation Logic with General Inductive Predicates. | Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, Jol Ouaknine |
| 2013 | CAV | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. | Christoph Haase, Samin Ishtiaq, Jol Ouaknine, Matthew J. Parkinson |
| 2013 | CONCUR | The Power of Priority Channel Systems. | Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen |
| 2013 | MFCS | Reachability in Register Machines with Polynomial Updates. | Alain Finkel, Stefan Gller, Christoph Haase |
| 2012 | FOSSACS | Branching-Time Model Checking of Parametric One-Counter Automata. | Stefan Gller, Christoph Haase, Jol Ouaknine, James Worrell |
| 2011 | CONCUR | Tractable Reasoning in a Fragment of Separation Logic. | Byron Cook, Christoph Haase, Jol Ouaknine, Matthew J. Parkinson, James Worrell |
| 2010 | ICALP | Model Checking Succinct and Parametric One-Counter Automata. | Stefan Gller, Christoph Haase, Jol Ouaknine, James Worrell |
| 2009 | CONCUR | Reachability in Succinct and Parametric One-Counter Automata. | Christoph Haase, Stephan Kreutzer, Jol Ouaknine, James Worrell |
| 2009 | ILP | Ideal Downward Refinement in the | Jens Lehmann, Christoph Haase |
| 2008 | ECAI | Complexity of Subsumption in the [Escr ][Lscr ] Family of Description Logics: Acyclic and Cyclic TBoxes. | Christoph Haase, Carsten Lutz |