Implementing RPO and POLO using SAT. - Peter Schneider-Kamp; Carsten Fuhs; René Thiemann; Jürgen Giesl; Elena Annov; Michael Codish; Aart Middeldorp; Harald Zankl (Deduction and Decision Procedures, 2007)

SAT Solving for Termination Analysis with Polynomial Interpretations. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (SAT, 2007)

Search Techniques for Rational Polynomial Orders. - Carsten Fuhs; Rafael Navarro-Marset; Carsten Otto; Jürgen Giesl; Salvador Lucas; Peter Schneider-Kamp (AISC/MKM/Calculemus, 2008)

Improving Context-Sensitive Dependency Pairs. - Beatriz Alarcón; Fabian Emmes; Carsten Fuhs; Jürgen Giesl; Raúl Gutiérrez; Salvador Lucas; Peter Schneider-Kamp; René Thiemann (LPAR, 2008)

Maximal Termination. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (RTA, 2008)

Termination Analysis by Dependency Pairs and Inductive Theorem Proving. - Stephan Swiderski; Michael Parting; Jürgen Giesl; Carsten Fuhs; Peter Schneider-Kamp (CADE, 2009)

Termination of Integer Term Rewriting. - Carsten Fuhs; Jürgen Giesl; Martin Plücker; Peter Schneider-Kamp; Stephan Falke 001 (Interaction versus Automation: The two Faces of Deduction, 2009)

Inductive Theorem Proving meets Dependency Pairs. - Stephan Swiderski; Michael Parting; Jürgen Giesl; Carsten Fuhs; Peter Schneider-Kamp (Interaction versus Automation: The two Faces of Deduction, 2009)

Proving Termination of Integer Term Rewriting. - Carsten Fuhs; Jürgen Giesl; Martin Plücker; Peter Schneider-Kamp; Stephan Falke 001 (RTA, 2009)

Lazy Abstraction for Size-Change Termination. - Michael Codish; Carsten Fuhs; Jürgen Giesl; Peter Schneider-Kamp (LPAR (Yogyakarta), 2010)

Optimizing the AES S-Box using SAT. - Carsten Fuhs; Peter Schneider-Kamp (IWIL@LPAR, 2010)

Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT. - Carsten Fuhs; Peter Schneider-Kamp (SAT, 2010)

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs. - Carsten Fuhs; Cynthia Kop (FroCoS, 2011)

Termination of Isabelle Functions via Termination of Rewriting. - Alexander Krauss 001; Christian Sternagel; René Thiemann; Carsten Fuhs; Jürgen Giesl (ITP, 2011)

A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. - Thomas Ströder; Fabian Emmes; Peter Schneider-Kamp; Jürgen Giesl; Carsten Fuhs (LOPSTR, 2011)

Optimal Base Encodings for Pseudo-Boolean Constraints. - Michael Codish; Yoav Fekete; Carsten Fuhs; Peter Schneider-Kamp (TACAS, 2011)

Proving Termination by Dependency Pairs and Inductive Theorem Proving. - Carsten Fuhs; Jürgen Giesl; Michael Parting; Peter Schneider-Kamp; Stephan Swiderski (J. Autom. Reason., 2011)

SAT-based termination analysis using monotonicity constraints over the integers. - Michael Codish; Igor Gonopolskiy; Amir M. Ben-Amram; Carsten Fuhs; Jürgen Giesl (Theory Pract. Log. Program., 2011)

Exotic Semi-Ring Constraints. - Michael Codish; Yoav Fekete; Carsten Fuhs; Jürgen Giesl; Johannes Waldmann (SMT@IJCAR, 2012)

Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. - Jürgen Giesl; Thomas Ströder; Peter Schneider-Kamp; Fabian Emmes; Carsten Fuhs (LOPSTR, 2012)

Polynomial Interpretations for Higher-Order Rewriting. - Carsten Fuhs; Cynthia Kop (RTA, 2012)

SAT encodings: from constraint-based termination analysis to circuit synthesis. - Carsten Fuhs (2012)

Better Termination Proving through Cooperation. - Marc Brockschmidt; Byron Cook; Carsten Fuhs (CAV, 2013)

Proving Termination of Programs Automatically with AProVE. - Jürgen Giesl; Marc Brockschmidt; Fabian Emmes; Florian Frohn; Carsten Fuhs; Carsten Otto; Martin Plücker; Peter Schneider-Kamp; Thomas Ströder; Stephanie Swiderski; René Thiemann (IJCAR, 2014)

Proving Termination and Memory Safety for Programs with Pointer Arithmetic. - Thomas Ströder; Jürgen Giesl; Marc Brockschmidt; Florian Frohn; Carsten Fuhs; Jera Hensel; Peter Schneider-Kamp (IJCAR, 2014)

A decision procedure for satisfiability in separation logic with inductive predicates. - James Brotherston; Carsten Fuhs; Juan Antonio Navarro Pérez; Nikos Gorogiannis (CSL-LICS, 2014)

Disproving termination with overapproximation. - Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (FMCAD, 2014)

First-Order Formative Rules. - Carsten Fuhs; Cynthia Kop (RTA-TLCA, 2014)

Alternating Runtime and Size Complexity Analysis of Integer Programs. - Marc Brockschmidt; Fabian Emmes; Stephan Falke 001; Carsten Fuhs; Jürgen Giesl (TACAS, 2014)

Proving Nontermination via Safety. - Hong Yi Chen; Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (TACAS, 2014)

Embracing Overapproximation for Proving Nontermination. - Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (Adv. Math. Commun., 2015)

Analyzing Runtime and Size Complexity of Integer Programs. - Marc Brockschmidt; Fabian Emmes; Stephan Falke 001; Carsten Fuhs; Jürgen Giesl (ACM Trans. Program. Lang. Syst., 2016)

Complexity Analysis for Term Rewriting by Integer Transition Systems. - Matthias Naaf; Florian Frohn; Marc Brockschmidt; Carsten Fuhs; Jürgen Giesl (FroCoS, 2017)

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). - Jasmin Christian Blanchette; Carsten Fuhs; Viorica Sofronie-Stokkermans; Cesare Tinelli (Dagstuhl Reports, 2017)

Analyzing Program Termination and Complexity Automatically with AProVE. - Jürgen Giesl; Cornelius Aschermann; Marc Brockschmidt; Fabian Emmes; Florian Frohn; Carsten Fuhs; Jera Hensel; Carsten Otto; Martin Plücker; Peter Schneider-Kamp; Thomas Ströder; Stephanie Swiderski; et al. (J. Autom. Reason., 2017)

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. - Thomas Ströder; Jürgen Giesl; Marc Brockschmidt; Florian Frohn; Carsten Fuhs; Jera Hensel; Peter Schneider-Kamp; Cornelius Aschermann (J. Autom. Reason., 2017)

Verifying Procedural Programs via Constrained Rewriting Induction. - Carsten Fuhs; Cynthia Kop; Naoki Nishida 001 (ACM Trans. Comput. Log., 2017)

The unified higher-order dependency pair framework. - Carsten Fuhs; Cynthia Kop (CoRR, 2018)

A Static Higher-Order Dependency Pair Framework. - Carsten Fuhs; Cynthia Kop (ESOP, 2019)

Transforming Derivational Complexity of Term Rewriting to Runtime Complexity. - Carsten Fuhs (FroCos, 2019)

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). - Carsten Fuhs; Philipp Rümmer; Renate A. Schmidt; Cesare Tinelli (Dagstuhl Reports, 2019)

Analysing Parallel Complexity of Term Rewriting. - Thaïs Baudon; Carsten Fuhs; Laure Gonnord (LOPSTR, 2022)

A calculus for modular loop acceleration and non-termination proofs. - Florian Frohn; Carsten Fuhs (Int. J. Softw. Tools Technol. Transf., 2022)

Proving Termination via Measure Transfer in Equivalence Checking. - Dragana Milovancevic; Carsten Fuhs; Mario Bucev; Viktor Kuncak (IFM, 2024)

On Complexity Bounds and Confluence of Parallel Term Rewriting. - Thaïs Baudon; Carsten Fuhs; Laure Gonnord (Fundam. Informaticae, 2024)

An Innermost DP Framework for Constrained Higher-Order Rewriting. - Carsten Fuhs; Liye Guo; Cynthia Kop (FSCD, 2025)