Christoph Haase

Latest

• An Efficient Quantifier Elimination Procedure for Presburger Arithmetic
• Integer Programming with GCD Constraints
• Reachability in Fixed VASS: Expressiveness and Lower Bounds
• Semënov Arithmetic, Affine VASS, and String Constraints
• Computing All Facts Entailed By An LTL Specification
• On Polynomial-Time Decidability of $k$-Negations Fragments of FO Theories (Extended Abstract)
• Universal quantification makes automatic structures hard to decide
• Geometric decision procedures and the VC dimension of linear arithmetic theories
• Quantifier elimination for counting extensions of Presburger arithmetic
• Higher-Order Quantified Boolean Satisfiability
• Affine Extensions of Integer Vector Addition Systems with States
• Directed Reachability for Infinite-State Systems
• On deciding linear arithmetic constraints over $p$-adic integers for all primes
• On the Expressiveness of Büchi Arithmetic
• The Reachability Problem for Two-Dimensional Vector Addition Systems with States
• Approaching Arithmetic Theories with Finite-State Automata
• On the power of ordering in linear arithmetic theories
• On the Size of Finite Rational Matrix Semigroups
• On the Existential Theories of Büchi Arithmetic and Linear $p$-adic Fields
• Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
• A survival guide to Presburger arithmetic
• Affine Extensions of Integer Vector Addition Systems with States
• Context-free commutative grammars with integer counters and resets
• Computing quantiles in Markov chains with multi-dimensional costs
• Counting Problems for Parikh Images
• Logics for continuous reachability in Petri nets and vector addition systems with states
• On the Complexity of Quantified Integer Programming
• The Logical View on Continuous Petri Nets
• A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
• Approaching the Coverability Problem Continuously
• Relating Reachability Problems in Timed and Counter Automata
• The complexity of the $K$th largest subset problem and related problems
• The Taming of the Semi-Linear Set
• Tightening the Complexity of Equivalence Problems for Commutative Grammars
• Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
• The Odds of Staying on Budget
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• Integer Vector Addition Systems with States
• Subclasses of Presburger arithmetic and the weak EXP hierarchy
• The Power of Priority Channel Systems
• Reachability in Register Machines with Polynomial Updates
• SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
• The Power of Priority Channel Systems
• Branching-Time Model Checking of Parametric One-Counter Automata
• On the Relationship between Reachability Problems in Timed and Counter Automata
• Tractable Reasoning in a Fragment of Separation Logic
• Model Checking Succinct and Parametric One-Counter Automata
• On Process-Algebraic Extensions of Metric Temporal Logic
• Ideal Downward Refinement in the $mathcalEL$ Description Logic
• Reachability in Succinct and Parametric One-Counter Automata
• Complexity of Subsumption in the $mathcalEL$ Family of Description Logics: Acyclic and Cyclic TBoxes