35 citations · 39 across the 8 of their papers we have counts for
10 papers
Beyond Absolute Positiveness for Universally Quantified Non-Linear Polynomial Constraints
Carsten Fuhs
Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for te…
On Complexity Bounds and Confluence of Parallel Term Rewriting
Thaïs Baudon, Carsten Fuhs, Laure Gonnord
We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in…
Analysing Parallel Complexity of Term Rewriting
Thaïs Baudon, Carsten Fuhs, Laure Gonnord
We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in…
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
Florian Frohn, Carsten Fuhs
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed.…
A static higher-order dependency pair framework
Carsten Fuhs, Cynthia Kop
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism desi…
The unified higher-order dependency pair framework
Carsten Fuhs, Cynthia Kop
In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the d…
Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…
First-Order Formative Rules
Carsten Fuhs, Cynthia Kop
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, for…
Polynomial Interpretations for Higher-Order Rewriting
Carsten Fuhs, Cynthia Kop
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recen…
Optimal Base Encodings for Pseudo-Boolean Constraints
Michael Codish, Yoav Fekete, Carsten Fuhs +1
This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrat…