35 citations · 169 across the 13 of their papers we have counts for
7 papers · 1 filter
Integer Programming with GCD Constraints
Rémy Defossez, Christoph Haase, Alessio Mansutti +1
We study the non-linear extension of integer programming with greatest common divisor constraints of the form , where and are linear polynomials, is a…
Semënov Arithmetic, Affine VASS, and String Constraints
Andrei Draghici, Christoph Haase, Florin Manea
We study extensions of Semënov arithmetic, the first-order theory of the structure . It is well-knonw that this theory becomes undecidable when extended with…
Universal quantification makes automatic structures hard to decide
Christoph Haase, Radoslaw Piórkowski
Automatic structures are first-order structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular lan…
Affine Extensions of Integer Vector Addition Systems with States
Michael Blondin, Christoph Haase, Filip Mazowiecki +1
We study the reachability problem for affine -VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the cou…
Approaching the Coverability Problem Continuously
Michael Blondin, Alain Finkel, Christoph Haase +1
The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challe…
Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
Christoph Haase
It is shown that for any fixed , the -fragment of Presburger arithmetic, i.e., its restriction to quantifier alternations beginning with an existential quantifi…
The Power of Priority Channel Systems
Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen
We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messag…