The Semantics of Rational Contractions. - Jürgen Giesl; Ingrid Neumann (EPIA, 1993)

Strategies for Semantical Contractions. - Jürgen Giesl; Ingrid Neumann (KI, 1994)

Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen. - Jürgen Giesl (Infix, 1995)

Automated Termination Proofs with Measure Functions. - Jürgen Giesl (KI, 1995)

Generating Polynomial Orderings for Termination Proofs. - Jürgen Giesl (RTA, 1995)

Termination Analysis for Functional Programs using Term Orderings - Jürgen Giesl (SAS, 1995)

Termination of Constructor Systems. - Thomas Arts; Jürgen Giesl (RTA, 1996)

Termination Analysis for Partial Functions. - Jürgen Brauburger; Jürgen Giesl (SAS, 1996)

Proving Innermost Normalisation Automatically. - Thomas Arts; Jürgen Giesl (RTA, 1997)

Automatically Proving Termination Where Simplification Orderings Fail. - Thomas Arts; Jürgen Giesl (TAPSOFT, 1997)

Termination of Nested and Mutually Recursive Algorithms. - Jürgen Giesl (J. Autom. Reason., 1997)

Termination Analysis by Inductive Evaluation. - Jürgen Brauburger; Jürgen Giesl (CADE, 1998)

Pushing the Frontiers of Combining Rewrite Systems Farther Outwards. - Jürgen Giesl; Enno Ohlebusch (FroCoS, 1998)

Modularity of Termination Using Dependency pairs. - Thomas Arts; Jürgen Giesl (RTA, 1998)

Applying Rewriting Techniques to the Verification of Erlang Processes. - Thomas Arts; Jürgen Giesl (CSL, 1999)

Context-Moving Transformations for Function Verification. - Jürgen Giesl (LOPSTR, 1999)

Transforming Context-Sensitive Rewrite Systems. - Jürgen Giesl; Aart Middeldorp (RTA, 1999)

Approximating the Domains of Functional and Imperative Programs. - Jürgen Brauburger; Jürgen Giesl (Sci. Comput. Program., 1999)

Eliminating Dummy Elimination. - Jürgen Giesl; Aart Middeldorp (CADE, 2000)

Equational Termination by Semantic Labelling. - Hitoshi Ohsaki; Aart Middeldorp; Jürgen Giesl (CSL, 2000)

Closure Induction in a Z-Like Language. - David A. Duffy; Jürgen Giesl (ZB, 2000)

Termination of term rewriting using dependency pairs. - Thomas Arts; Jürgen Giesl (Theor. Comput. Sci., 2000)

Decidable Classes of Inductive Theorems. - Jürgen Giesl; Deepak Kapur (IJCAR, 2001)

Dependency Pairs for Equational Rewriting. - Jürgen Giesl; Deepak Kapur (RTA, 2001)

Verification of Erlang Processes by Dependency Pairs. - Jürgen Giesl; Thomas Arts (Appl. Algebra Eng. Commun. Comput., 2001)

Special Issue "Termination". - Jürgen Giesl; Pierre Lescanne (Appl. Algebra Eng. Commun. Comput., 2001)

Induction Proofs with Partial Functions. - Jürgen Giesl (J. Autom. Reason., 2001)

Innermost Termination of Context-Sensitive Rewriting. - Jürgen Giesl; Aart Middeldorp (Developments in Language Theory, 2002)

Modular Termination Proofs for Rewriting Using Dependency Pairs. - Jürgen Giesl; Thomas Arts; Enno Ohlebusch (J. Symb. Comput., 2002)

Deaccumulation - Improving Provability. - Jürgen Giesl; Armin Kühnemann; Janis Voigtländer (ASIAN, 2003)

Deciding Inductive Validity of Equations. - Jürgen Giesl; Deepak Kapur (CADE, 2003)

Improving Dependency Pairs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (LPAR, 2003)

Liveness in Rewriting. - Jürgen Giesl; Hans Zantema (RTA, 2003)

Size-Change Termination for Term Rewriting. - René Thiemann; Jürgen Giesl (RTA, 2003)

Simulating liveness by reduction strategies. - Jürgen Giesl; Hans Zantema (WRS, 2003)

Improved Modular Termination Proofs Using Dependency Pairs. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (IJCAR, 2004)

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (LPAR, 2004)

Automated Termination Proofs with AProVE. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (RTA, 2004)

Transformation techniques for context-sensitive rewrite systems. - Jürgen Giesl; Aart Middeldorp (J. Funct. Program., 2004)

Proving and Disproving Termination in the Dependency Pair Framework. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (Deduction and Applications, 2005)

Proving and Disproving Termination of Higher-Order Functions. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (FroCoS, 2005)

The size-change principle and dependency pairs for termination of term rewriting. - René Thiemann; Jürgen Giesl (Appl. Algebra Eng. Commun. Comput., 2005)

Preface. - Jürgen Giesl; Deepak Kapur (J. Autom. Reason., 2005)

Automatic Termination Proofs in the Dependency Pair Framework. - Jürgen Giesl; Peter Schneider-Kamp; René Thiemann (IJCAR, 2006)

Automated Termination Analysis for Logic Programs by Term Rewriting. - Peter Schneider-Kamp; Jürgen Giesl; Alexander Serebrenik; René Thiemann (LOPSTR, 2006)

SAT Solving for Argument Filterings. - Michael Codish; Peter Schneider-Kamp; Vitaly Lagoon; René Thiemann; Jürgen Giesl (LPAR, 2006)

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. - Jürgen Giesl; Stephan Swiderski; Peter Schneider-Kamp; René Thiemann (RTA, 2006)

Third Special Issue on Techniques for Automated Termination Proofs. - Jürgen Giesl; Deepak Kapur (J. Autom. Reason., 2006)

Mechanizing and Improving Dependency Pairs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (J. Autom. Reason., 2006)

Proving Termination by Bounded Increase. - Jürgen Giesl; René Thiemann; Stephan Swiderski; Peter Schneider-Kamp (CADE, 2007)

07401 Executive Summary – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

07401 Abstracts Collection – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

Termination of Programs using Term Rewriting and SAT Solving. - Jürgen Giesl; Peter Schneider-Kamp; René Thiemann; Stephan Swiderski; Manh Thang Nguyen; Danny De Schreye; Alexander Serebrenik (Deduction and Decision Procedures, 2007)

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)

Decision Procedures for Loop Detection. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (Deduction and Decision Procedures, 2007)

Proving Termination Using Recursive Path Orders and SAT Solving. - Peter Schneider-Kamp; René Thiemann; Elena Annov; Michael Codish; Jürgen Giesl (FroCoS, 2007)

Termination Analysis of Logic Programs Based on Dependency Graphs. - Manh Thang Nguyen; Jürgen Giesl; Peter Schneider-Kamp; Danny De Schreye (LOPSTR, 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)

Preface. - Jürgen Giesl (WRS@RDP, 2007)

RTA 2005. - Jürgen Giesl (Inf. Comput., 2007)

Deaccumulation techniques for improving provability. - Jürgen Giesl; Armin Kühnemann; Janis Voigtländer (J. Log. Algebraic Methods Program., 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)

Deciding Innermost Loops. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (RTA, 2008)

Adding constants to string rewriting. - René Thiemann; Hans Zantema; Jürgen Giesl; Peter Schneider-Kamp (Appl. Algebra Eng. Commun. Comput., 2008)

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

09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction. - Thomas Ball 001; Jürgen Giesl; Reiner Hähnle; Tobias Nipkow (Interaction versus Automation: The two Faces of Deduction, 2009)

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions. - Thomas Ball 001; Jürgen Giesl; Reiner Hähnle; Tobias Nipkow (Interaction versus Automation: The two Faces of Deduction, 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)

The Dependency Triple Framework for Termination of Logic Programs. - Peter Schneider-Kamp; Jürgen Giesl; Manh Thang Nguyen (LOPSTR, 2009)

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

Automated termination proofs for logic programs by term rewriting. - Peter Schneider-Kamp; Jürgen Giesl; Alexander Serebrenik; René Thiemann (ACM Trans. Comput. Log., 2009)

Termination Graphs for Java Bytecode. - Marc Brockschmidt; Carsten Otto; Christian von Essen; Jürgen Giesl (Verification, Induction, Termination Analysis, 2010)

Dependency Triples for Improving Termination Analysis of Logic Programs with Cut. - Thomas Ströder; Peter Schneider-Kamp; Jürgen Giesl (LOPSTR, 2010)

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

Automated Termination Analysis of Java Bytecode by Term Rewriting. - Carsten Otto; Marc Brockschmidt; Christian von Essen; Jürgen Giesl (RTA, 2010)

Loops under Strategies ... Continued - René Thiemann; Christian Sternagel; Jürgen Giesl; Peter Schneider-Kamp (IWS, 2010)

Special Issue on Automated Deduction. - Jürgen Giesl (Künstliche Intell., 2010)

Current Trends in Automated Deduction. - Jürgen Giesl (Künstliche Intell., 2010)

Automated termination analysis for logic programs with cut. - Peter Schneider-Kamp; Jürgen Giesl; Thomas Ströder; Alexander Serebrenik; René Thiemann (Theory Pract. Log. Program., 2010)

A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. - Lars Noschinski; Fabian Emmes; Jürgen Giesl (CADE, 2011)

Automated Detection of Non-termination and NullPointerExceptions for Java Bytecode. - Marc Brockschmidt; Thomas Ströder; Carsten Otto; Jürgen Giesl (FoVeOOS, 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)

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting. - Marc Brockschmidt; Carsten Otto; Jürgen Giesl (RTA, 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)

Preface: Special Issue of Selected Extended Papers of IJCAR 2010. - Jürgen Giesl; Reiner Hähnle (J. Autom. Reason., 2011)

Automated termination proofs for haskell by term rewriting. - Jürgen Giesl; Matthias Raffelsieper; Peter Schneider-Kamp; Stephan Swiderski; René Thiemann (ACM Trans. Program. Lang. Syst., 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)

Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. - Manh Thang Nguyen; Danny De Schreye; Jürgen Giesl; Peter Schneider-Kamp (Theory Pract. Log. Program., 2011)

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

Proving Non-looping Non-termination Automatically. - Fabian Emmes; Tim Enger; Jürgen Giesl (IJCAR, 2012)

Automated Termination Proofs for Java Programs with Cyclic Data. - Marc Brockschmidt; Richard Musiol; Carsten Otto; Jürgen Giesl (CAV, 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)

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. - Michael Codish; Jürgen Giesl; Peter Schneider-Kamp; René Thiemann (J. Autom. Reason., 2012)

Automated Termination Analysis: From Term Rewriting to Programming Languages. - Jürgen Giesl (Software Engineering (Workshops), 2013)

Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. - Lars Noschinski; Fabian Emmes; Jürgen Giesl (J. Autom. Reason., 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)

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

Termination Competition (termCOMP 2015). - Jürgen Giesl; Frédéric Mesnard; Albert Rubio; René Thiemann; Johannes Waldmann (CADE, 2015)

Inferring Lower Bounds for Runtime Complexity. - Florian Frohn; Jürgen Giesl; Jera Hensel; Cornelius Aschermann; Thomas Ströder (RTA, 2015)

AProVE: Termination and Memory Safety of C Programs - (Competition Contribution). - Thomas Ströder; Cornelius Aschermann; Florian Frohn; Jera Hensel; Jürgen Giesl (TACAS, 2015)

Lower Runtime Bounds for Integer Programs. - Florian Frohn; Matthias Naaf; Jera Hensel; Marc Brockschmidt; Jürgen Giesl (IJCAR, 2016)

Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution. - Jera Hensel; Jürgen Giesl; Florian Frohn; Thomas Ströder (SEFM, 2016)

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)

Complexity Analysis for Java with AProVE. - Florian Frohn; Jürgen Giesl (IFM, 2017)

Analyzing Runtime Complexity via Innermost Runtime Complexity. - Florian Frohn; Jürgen Giesl (LPAR, 2017)

AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution). - Jera Hensel; Frank Emrich; Florian Frohn; Thomas Ströder; Jürgen Giesl (TACAS (2), 2017)

Lower Bounds for Runtime Complexity of Term Rewriting. - Florian Frohn; Jürgen Giesl; Jera Hensel; Cornelius Aschermann; Thomas Ströder (J. Autom. Reason., 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)

Preface: Special Issue on Automatic Resource Bound Analysis. - Jürgen Giesl; Jan Hoffmann 002 (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)

Constant runtime complexity of term rewriting is semi-decidable. - Florian Frohn; Jürgen Giesl (Inf. Process. Lett., 2018)

Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution. - Jera Hensel; Jürgen Giesl; Florian Frohn; Thomas Ströder (J. Log. Algebraic Methods Program., 2018)

Computing Expected Runtimes for Constant Probability Programs. - Jürgen Giesl; Peter Giesl; Marcel Hark (CADE, 2019)

Termination of Triangular Integer Loops is Decidable. - Florian Frohn; Jürgen Giesl (CAV (2), 2019)

Proving Non-Termination via Loop Acceleration. - Florian Frohn; Jürgen Giesl (FMCAD, 2019)

The Termination and Complexity Competition. - Jürgen Giesl; Albert Rubio; Christian Sternagel; Johannes Waldmann; Akihisa Yamada 002 (TACAS (3), 2019)

Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (CoRR, 2019)

On the Decidability of Termination for Polynomial Loops. - Florian Frohn; Marcel Hark; Jürgen Giesl (CoRR, 2019)

Polynomial Loops: Beyond Termination. - Marcel Hark; Florian Frohn; Jürgen Giesl (LPAR, 2020)

Termination of Polynomial Loops. - Florian Frohn; Marcel Hark; Jürgen Giesl (SAS, 2020)

Aiming low is harder: induction for lower bounds in probabilistic program verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2020)

Inferring Lower Runtime Bounds for Integer Programs. - Florian Frohn; Matthias Naaf; Marc Brockschmidt; Jürgen Giesl (ACM Trans. Program. Lang. Syst., 2020)

Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. - Fabian Meyer; Marcel Hark; Jürgen Giesl (TACAS (1), 2021)

Improving Automatic Complexity Analysis of Integer Programs. - Jürgen Giesl; Nils Lommen; Marcel Hark; Fabian Meyer (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). - Florian Frohn; Jürgen Giesl (IJCAR, 2022)

Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops. - Nils Lommen; Fabian Meyer; Jürgen Giesl (IJCAR, 2022)

AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution). - Jera Hensel; Constantin Mensendiek; Jürgen Giesl (TACAS (2), 2022)

Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). - Florian Frohn; Jürgen Giesl (CADE, 2023)

Proving Termination of C Programs with Lists. - Jera Hensel; Jürgen Giesl (CADE, 2023)

Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. - Jan-Christoph Kassing; Jürgen Giesl (CADE, 2023)

Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs. - Nils Lommen; Jürgen Giesl (FroCoS, 2023)

ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses. - Florian Frohn; Jürgen Giesl (SAS, 2023)

AProVE: Modular Termination Analysis of Memory-Manipulating C Programs. - Frank Emrich; Jera Hensel; Jürgen Giesl (CoRR, 2023)

Proving Non-Termination by Acceleration Driven Clause Learning with LoAT. - Florian Frohn; Jürgen Giesl (CoRR, 2023)

Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version). - Florian Frohn; Jürgen Giesl (CoRR, 2023)

Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version). - Jan-Christoph Kassing; Jürgen Giesl (CoRR, 2023)

Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (Short WST Version). - Nils Lommen; Eleanore Meyer; Jürgen Giesl (CoRR, 2023)

Automated Termination Proofs for C Programs with Lists (Short WST Version). - Jera Hensel; Jürgen Giesl (CoRR, 2023)

Improving Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Jürgen Giesl (CoRR, 2023)

Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Jürgen Giesl (Principles of Verification (1), 2024)

A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Stefan Dollase; Jürgen Giesl (FLOPS, 2024)

Integrating Loop Acceleration Into Bounded Model Checking. - Florian Frohn; Jürgen Giesl (FM (1), 2024)

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Florian Frohn; Jürgen Giesl (FoSSaCS (2), 2024)

On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. - Franz Baader; Jürgen Giesl (FSCD, 2024)

Satisfiability Modulo Exponential Integer Arithmetic. - Florian Frohn; Jürgen Giesl (IJCAR (1), 2024)

A Dependency Pair Framework for Relative Termination of Term Rewriting. - Jan-Christoph Kassing; Grigory Vartanyan; Jürgen Giesl (IJCAR (2), 2024)

Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper) - (Short Paper). - Nils Lommen; Éléanore Meyer; Jürgen Giesl (IJCAR (1), 2024)

Accelerated Bounded Model Checking. - Florian Frohn; Jürgen Giesl (CoRR, 2024)

Control-Flow Refinement for Probabilistic Programs in KoAT. - Nils Lommen; Éléanore Meyer; Jürgen Giesl (CoRR, 2024)

From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity. - Jan-Christoph Kassing; Jürgen Giesl (CoRR, 2024)

Targeting Completeness: Automated Complexity Analysis of Integer Programs. - Nils Lommen; Éléanore Meyer; Jürgen Giesl (CoRR, 2024)

Small Term Reachability and Related Problems for Terminating Term Rewriting Systems. - Franz Baader; Jürgen Giesl (CoRR, 2024)

The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Jürgen Giesl (CoRR, 2024)

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting - AProVE Artifact. - Jan-Christoph Kassing; Florian Frohn; Jürgen Giesl (Zenodo, 2024)

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting - AProVE Artifact. - Jan-Christoph Kassing; Florian Frohn; Jürgen Giesl (Zenodo, 2024)

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting - AProVE Artifact. - Jan-Christoph Kassing; Florian Frohn; Jürgen Giesl (Zenodo, 2024)

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting - AProVE Artifact. - Jan-Christoph Kassing; Florian Frohn; Jürgen Giesl (Zenodo, 2024)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2024)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2024)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2024)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2024)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2024)

Infinite State Model Checking by Learning Transitive Relations. - Florian Frohn; Jürgen Giesl (CADE, 2025)

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. - Emma Ahrens; Jan-Christoph Kassing; Jürgen Giesl; Joost-Pieter Katoen (FSCD, 2025)

Deciding Termination of Simple Randomized Loops. - Éléanore Meyer; Jürgen Giesl (MFCS, 2025)

AProVE(KoAT+LoAT) - (Competition Contribution). - Nils Lommen; Jürgen Giesl (TACAS (3), 2025)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2025)

Termination of triangular polynomial loops. - Marcel Hark; Florian Frohn; Jürgen Giesl (Formal Methods Syst. Des., 2025)

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting. - Jan-Christoph Kassing; Leon Spitzer; Jürgen Giesl (CoRR, 2025)

AProVE (KoAT + LoAT). - Nils Lommen; Jürgen Giesl (Zenodo, 2025)