@inproceedings{BHO21,
  title = "Directed Reachability for Infinite-State Systems",
  author = "Michael Blondin and Christoph Haase and Philip Offtermatt",
  year = "2021",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, {TACAS}",
  note = "To appear",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
}
@inproceedings{HR21,
  title = "On the Expressiveness of {B}{\"u}chi Arithmetic",
  author = "Christoph Haase and Jakub R{\'o}{\.{z}}ycki",
  year = "2021",
  booktitle = "Foundations of Software Science and Computation Structures, {FOSSACS}",
  note = "To appear",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
}
@inproceedings{Haa20,
  title = "Approaching Arithmetic Theories with Finite-State Automata",
  author = "Christoph Haase",
  year = "2020",
  booktitle = "Language and Automata Theory and Applications, {LATA}",
  pages = "1--11",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "12038",
  doi = "10.1007/978-3-030-40608-0_3",
}
@inproceedings{CH20,
  title = "On the power of ordering in linear arithmetic theories",
  author = "Dmitry Chistikov and Christoph Haase",
  year = "2020",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "119:1--119:15",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "168",
  doi = "10.4230/LIPIcs.ICALP.2020.119",
}
@inproceedings{BHKST20,
  title = "On the Size of Finite Rational Matrix Semigroups",
  author = "Georgina Bumpus and Christoph Haase and Stefan Kiefer and Paul-Ioan Stoienescu and Jonathan Tanner",
  year = "2020",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "115:1--115:13",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "168",
  doi = "10.4230/LIPIcs.ICALP.2020.115",
}
@inproceedings{GHW19,
  title = "On the Existential Theories of {B}\"uchi Arithmetic and Linear $p$-adic Fields",
  author = "Florent Gu\'epin and Christoph Haase and James Worrell",
  year = "2019",
  booktitle = "Logic in Computer Science, {LICS}",
  publisher = "IEEE",
  doi = "10.1109/LICS.2019.8785681",
}
@inproceedings{HZ19,
  title = "Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests",
  author = "Christoph Haase and Georg Zetzsche",
  year = "2019",
  booktitle = "Logic in Computer Science, {LICS}",
  publisher = "IEEE",
  doi = "10.1109/LICS.2019.8785850",
}
@article{CHH18,
  title = "Context-free commutative grammars with integer counters and resets",
  author = "Dmitry Chistikov and Christoph Haase and Simon Halfon",
  year = "2018",
  journal = "Theor. Comput. Sci.",
  pages = "147--161",
  volume = "735",
  doi = "10.1016/j.tcs.2016.06.017",
}
@inproceedings{BHM18,
  title = "Affine Extensions of Integer Vector Addition Systems with States",
  author = "Michael Blondin and Christoph Haase and Filip Mazowiecki",
  year = "2018",
  booktitle = "Concurrency Theory, {CONCUR}",
  pages = "14:1--14:17",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "118",
  doi = "10.4230/LIPIcs.CONCUR.2018.14",
}
@article{Haa18,
  title = "A survival guide to {P}resburger arithmetic",
  author = "Christoph Haase",
  year = "2018",
  journal = "{SIGLOG} News",
  number = "3",
  pages = "67--82",
  volume = "5",
  doi = "10.1145/3242953.3242964",
}
@inproceedings{HKL17b,
  title = "Counting Problems for Parikh Images",
  author = "Christoph Haase and Stefan Kiefer and Markus Lohrey",
  year = "2017",
  booktitle = "Mathematical Foundations of Computer Science, {MFCS}",
  pages = "12:1--12:13",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "83",
  doi = "10.4230/LIPIcs.MFCS.2017.12",
}
@inproceedings{BH17,
  title = "Logics for continuous reachability in {P}etri nets and vector addition systems with states",
  author = "Michael Blondin and Christoph Haase",
  year = "2017",
  booktitle = "Logic in Computer Science, {LICS}",
  publisher = "IEEE",
  doi = "10.1109/LICS.2017.8005068",
}
@article{BFHH17,
  title = "The Logical View on Continuous {P}etri Nets",
  author = "Michael Blondin and Alain Finkel and Christoph Haase and Serge Haddad",
  year = "2017",
  journal = "{ACM} Trans. Comput. Log.",
  number = "3",
  pages = "24:1--24:28",
  volume = "18",
  doi = "10.1145/3105908",
}
@inproceedings{HKL17,
  title = "Computing quantiles in {M}arkov chains with multi-dimensional costs",
  author = "Christoph Haase and Stefan Kiefer and Markus Lohrey",
  year = "2017",
  booktitle = "Logic in Computer Science, {LICS}",
  publisher = "IEEE",
  doi = "10.1109/LICS.2017.8005090",
}
@inproceedings{CH17,
  title = "On the Complexity of Quantified Integer Programming",
  author = "Dmitry Chistikov and Christoph Haase",
  year = "2017",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "94:1--94:13",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "80",
  doi = "10.4230/LIPIcs.ICALP.2017.94",
}
@article{HOW16,
  title = "Relating Reachability Problems in Timed and Counter Automata",
  author = "Christoph Haase and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2016",
  journal = "Fundam. Inform.",
  number = "3-4",
  pages = "317--338",
  volume = "143",
  doi = "10.3233/FI-2016-1316",
}
@inproceedings{GHLT16,
  title = "A Polynomial-Time Algorithm for Reachability in Branching {VASS} in Dimension One",
  author = "Stefan G{\"{o}}ller and Christoph Haase and Ranko Lazic and Patrick Totzke",
  year = "2016",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "105:1--105:13",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "55",
  doi = "10.4230/LIPIcs.ICALP.2016.105",
}
@inproceedings{BFHH16,
  title = "Approaching the Coverability Problem Continuously",
  author = "Michael Blondin and Alain Finkel and Christoph Haase and Serge Haddad",
  year = "2016",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, {TACAS}",
  pages = "480--496",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "9636",
  doi = "10.1007/978-3-662-49674-9\_28",
}
@article{HK16,
  title = "The complexity of the $K$th largest subset problem and related problems",
  author = "Christoph Haase and Stefan Kiefer",
  year = "2016",
  journal = "Inf. Process. Lett.",
  number = "2",
  pages = "111--115",
  volume = "116",
  doi = "10.1016/j.ipl.2015.09.015",
}
@inproceedings{HH16,
  title = "Tightening the Complexity of Equivalence Problems for Commutative Grammars",
  author = "Christoph Haase and Piotr Hofman",
  year = "2016",
  booktitle = "Symposium on Theoretical Aspects of Computer Science, {STACS}",
  pages = "41:1--41:14",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "47",
  doi = "10.4230/LIPIcs.STACS.2016.41",
}
@inproceedings{CH16,
  title = "The Taming of the Semi-Linear Set",
  author = "Dmitry Chistikov and Christoph Haase",
  year = "2016",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "128:1--128:13",
  publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",
  series = "LIPIcs",
  volume = "55",
  doi = "10.4230/LIPIcs.ICALP.2016.128",
}
@inproceedings{BFGHM15,
  title = "Reachability in Two-Dimensional Vector Addition Systems with States Is {PSPACE}-Complete",
  author = "Michael Blondin and Alain Finkel and Stefan G{\"{o}}ller and Christoph Haase and Pierre McKenzie",
  year = "2015",
  booktitle = "Logic in Computer Science, {LICS}",
  pages = "32--43",
  publisher = "IEEE",
  doi = "10.1109/LICS.2015.14",
}
@inproceedings{HK15,
  title = "The Odds of Staying on Budget",
  author = "Christoph Haase and Stefan Kiefer",
  year = "2015",
  booktitle = "Automata, Languages, and Programming, {ICALP}",
  pages = "234--246",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "9135",
  doi = "10.1007/978-3-662-47666-6\_19",
}
@article{HSS14,
  title = "The Power of Priority Channel Systems",
  author = "Christoph Haase and Sylvain Schmitz and Philippe Schnoebelen",
  year = "2014",
  journal = "Log. Methods Comput. Sci.",
  number = "4",
  volume = "10",
  doi = "10.2168/LMCS-10(4:4)2014",
}
@inproceedings{HH14,
  title = "Integer Vector Addition Systems with States",
  author = "Christoph Haase and Simon Halfon",
  year = "2014",
  booktitle = "Reachability Problems, {RP}",
  pages = "112--124",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "8762",
  doi = "10.1007/978-3-319-11439-2\_9",
}
@inproceedings{AGHKO14,
  title = "Foundations for Decision Problems in Separation Logic with General Inductive Predicates",
  author = "Timos Antonopoulos and Nikos Gorogiannis and Christoph Haase and Max I. Kanovich and Jo{\"{e}}l Ouaknine",
  year = "2014",
  booktitle = "Foundations of Software Science and Computation Structures, {FOSSACS}",
  pages = "411--425",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "8412",
  doi = "10.1007/978-3-642-54830-7\_27",
}
@inproceedings{Haa14,
  title = "Subclasses of {P}resburger arithmetic and the weak {EXP} hierarchy",
  author = "Christoph Haase",
  year = "2014",
  booktitle = "Computer Science Logic and Logic in Computer Science, {CSL-LICS}",
  pages = "47:1--47:10",
  publisher = "ACM",
  doi = "10.1145/2603088.2603092",
}
@inproceedings{FGH13,
  title = "Reachability in Register Machines with Polynomial Updates",
  author = "Alain Finkel and Stefan G{\"{o}}ller and Christoph Haase",
  year = "2013",
  booktitle = "Mathematical Foundations of Computer Science, {MFCS}",
  pages = "409--420",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "8087",
  doi = "10.1007/978-3-642-40313-2\_37",
}
@inproceedings{HSS13,
  title = "The Power of Priority Channel Systems",
  author = "Christoph Haase and Sylvain Schmitz and Philippe Schnoebelen",
  year = "2013",
  booktitle = "Concurrency Theory, {CONCUR}",
  pages = "319--333",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "8052",
  doi = "10.1007/978-3-642-40184-8\_23",
}
@inproceedings{HIOP13,
  title = "SeLoger: {A} Tool for Graph-Based Reasoning in Separation Logic",
  author = "Christoph Haase and Samin Ishtiaq and Jo{\"{e}}l Ouaknine and Matthew J. Parkinson",
  year = "2013",
  booktitle = "Computer Aided Verification, {CAV}",
  pages = "790--795",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "8044",
  doi = "10.1007/978-3-642-39799-8\_55",
}
@inproceedings{HOW12,
  title = "On the Relationship between Reachability Problems in Timed and Counter Automata",
  author = "Christoph Haase and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2012",
  booktitle = "Reachability Problems, {RP}",
  pages = "54--65",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "7550",
  doi = "10.1007/978-3-642-33512-9\_6",
}
@inproceedings{GHOW12,
  title = "Branching-Time Model Checking of Parametric One-Counter Automata",
  author = "Stefan G{\"{o}}ller and Christoph Haase and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2012",
  booktitle = "Foundations of Software Science and Computational Structures, {FOSSACS}",
  pages = "406--420",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "7213",
  doi = "10.1007/978-3-642-28729-9\_27",
}
@inproceedings{CHOPW11,
  title = "Tractable Reasoning in a Fragment of Separation Logic",
  author = "Byron Cook and Christoph Haase and Jo{\"{e}}l Ouaknine and Matthew J. Parkinson and James Worrell",
  year = "2011",
  booktitle = "Concurrency Theory, {CONCUR}",
  pages = "235--249",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "6901",
  doi = "10.1007/978-3-642-23217-6\_16",
}
@incollection{HOW10,
  title = "On Process-Algebraic Extensions of Metric Temporal Logic",
  author = "Christoph Haase and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2010",
  booktitle = "Reflections on the Work of C. A. R. Hoare.",
  isbn = "978-1-84882-911-4",
  pages = "283--300",
  publisher = "Springer",
  doi = "10.1007/978-1-84882-912-1\_13",
}
@inproceedings{GHOW10,
  title = "Model Checking Succinct and Parametric One-Counter Automata",
  author = "Stefan G{\"{o}}ller and Christoph Haase and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2010",
  booktitle = "Automata, Languages and Programming, {ICALP}",
  pages = "575--586",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "6199",
  doi = "10.1007/978-3-642-14162-1\_48",
}
@inproceedings{LH09,
  title = "Ideal Downward Refinement in the $\mathcal{EL}$ Description Logic",
  author = "Jens Lehmann and Christoph Haase",
  year = "2009",
  booktitle = "Inductive Logic Programming, {ILP}",
  pages = "73--87",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  url = "https://doi.org/10.1007/978-3-642-13840-9\_8",
  volume = "5989",
  doi = "10.1007/978-3-642-13840-9\_8",
}
@inproceedings{HKOW09,
  title = "Reachability in Succinct and Parametric One-Counter Automata",
  author = "Christoph Haase and Stephan Kreutzer and Jo{\"{e}}l Ouaknine and James Worrell",
  year = "2009",
  booktitle = "Concurrency Theory, {CONCUR}",
  pages = "369--383",
  publisher = "Springer",
  series = "Lect. Notes Comp. Sci.",
  volume = "5710",
  doi = "10.1007/978-3-642-04081-8\_25",
}
@inproceedings{HL08,
  title = "Complexity of Subsumption in the $\mathcal{EL}$ Family of Description Logics: Acyclic and Cyclic {TB}oxes",
  author = "Christoph Haase and Carsten Lutz",
  year = "2008",
  booktitle = "European Conference on Artificial Intelligence, {ECAI}",
  pages = "25--29",
  publisher = "{IOS} Press",
  series = "Frontiers in Artificial Intelligence and Applications",
  volume = "178",
  doi = "10.3233/978-1-58603-891-5-25",
}