42 citations · 161 across the 23 of their papers we have counts for
6 papers · 1 filter
On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
Christoph Haase, Alessio Mansutti, Amaury Pouly
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that…
The Membership Problem for Hypergeometric Sequences with Rational Parameters
Klara Nosan, Amaury Pouly, Mahsa Shirmohammadi +1
We investigate the Membership Problem for hypergeometric sequences: given a hypergeometric sequence of rational numbers and a target $t \in \math…
On the Monniaux Problem in Abstract Interpretation
Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann +3
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program , a safety (\emph{e.g.}, non-reachability) s…
Algebraic Invariants for Linear Hybrid Automata
Rupak Majumdar, Joël Ouaknine, Amaury Pouly +1
We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given unguarded linear hybrid automaton (i.e., a hybrid automa…
Polynomial Invariants for Affine Programs
Ehud Hrushovski, Joël Ouaknine, Amaury Pouly +1
We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-determin…
Model Checking Flat Freeze LTL on One-Counter Automata
Antonia Lechner, Richard Mayr, Joël Ouaknine +2
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-coun…