| 2026 | CAV | KoAT: Automatic Complexity and Termination Analysis of Integer Programs. | Nils Lommen, lanore Meyer, Jrgen Giesl |
| 2026 | ESOP | Modular Automatic Complexity Analysis of Recursive Integer Programs. | Nils Lommen, Jrgen Giesl |
| 2026 | IJCAR | Accelerating Loops with Arrays. | Florian Frohn, Jrgen Giesl |
| 2026 | IJCAR | Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks. | Jan-Christoph Kassing, Henri Nagel, Alexander Schlecht, Jrgen Giesl |
| 2026 | TACAS | On Deciding Constant Runtime of Linear Loops. | Florian Frohn, Jrgen Giesl, Peter Giesl, Nils Lommen |
| 2025 | CADE | Infinite State Model Checking by Learning Transitive Relations. | Florian Frohn, Jrgen Giesl |
| 2025 | FSCD | Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. | Emma Ahrens, Jan-Christoph Kassing, Jrgen Giesl, Joost-Pieter Katoen |
| 2025 | MFCS | Deciding Termination of Simple Randomized Loops. | lanore Meyer, Jrgen Giesl |
| 2025 | PPDP | Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting. | Jan-Christoph Kassing, Leon Valentin Spitzer, Jrgen Giesl |
| 2025 | TACAS | AProVE(KoAT+LoAT) - (Competition Contribution). | Nils Lommen, Jrgen Giesl |
| 2024 | FLOPS | A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting. | Jan-Christoph Kassing, Stefan Dollase, Jrgen Giesl |
| 2024 | FM | Integrating Loop Acceleration Into Bounded Model Checking. | Florian Frohn, Jrgen Giesl |
| 2024 | FOSSACS | From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting. | Jan-Christoph Kassing, Florian Frohn, Jrgen Giesl |
| 2024 | FSCD | On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. | Franz Baader, Jrgen Giesl |
| 2024 | IJCAR | Satisfiability Modulo Exponential Integer Arithmetic. | Florian Frohn, Jrgen Giesl |
| 2024 | IJCAR | A Dependency Pair Framework for Relative Termination of Term Rewriting. | Jan-Christoph Kassing, Grigory Vartanyan, Jrgen Giesl |
| 2024 | IJCAR | Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper) - (Short Paper). | Nils Lommen, lanore Meyer, Jrgen Giesl |
| 2023 | CADE | Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). | Florian Frohn, Jrgen Giesl |
| 2023 | CADE | Proving Termination of C Programs with Lists. | Jera Hensel, Jrgen Giesl |
| 2023 | CADE | Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. | Jan-Christoph Kassing, Jrgen Giesl |
| 2023 | SAS | ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses. | Florian Frohn, Jrgen Giesl |
| 2022 | CADE | Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). | Florian Frohn, Jrgen Giesl |
| 2022 | CADE | Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops. | Nils Lommen, Fabian Meyer, Jrgen Giesl |
| 2022 | TACAS | AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution). | Jera Hensel, Constantin Mensendiek, Jrgen Giesl |
| 2021 | TACAS | Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. | Fabian Meyer, Marcel Hark, Jrgen Giesl |
| 2020 | LPAR | Polynomial Loops: Beyond Termination. | Marcel Hark, Florian Frohn, Jrgen Giesl |
| 2020 | SAS | Termination of Polynomial Loops. | Florian Frohn, Marcel Hark, Jrgen Giesl |
| 2019 | CADE | Computing Expected Runtimes for Constant Probability Programs. | Jrgen Giesl, Peter Giesl, Marcel Hark |
| 2019 | CAV | Termination of Triangular Integer Loops is Decidable. | Florian Frohn, Jrgen Giesl |
| 2019 | FMCAD | Proving Non-Termination via Loop Acceleration. | Florian Frohn, Jrgen Giesl |
| 2019 | TACAS | The Termination and Complexity Competition. | Jrgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada |
| 2017 | IFM | Complexity Analysis for Java with AProVE. | Florian Frohn, Jrgen Giesl |
| 2017 | LPAR | Analyzing Runtime Complexity via Innermost Runtime Complexity. | Florian Frohn, Jrgen Giesl |
| 2017 | TACAS | AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution). | Jera Hensel, Frank Emrich, Florian Frohn, Thomas Strder, Jrgen Giesl |
| 2016 | CADE | Lower Runtime Bounds for Integer Programs. | Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, Jrgen Giesl |
| 2016 | SEFM | Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution. | Jera Hensel, Jrgen Giesl, Florian Frohn, Thomas Strder |
| 2015 | CADE | Termination Competition (termCOMP 2015). | Jrgen Giesl, Frdric Mesnard, Albert Rubio, Ren Thiemann, Johannes Waldmann |
| 2015 | TACAS | AProVE: Termination and Memory Safety of C Programs - (Competition Contribution). | Thomas Strder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jrgen Giesl |
| 2014 | CADE | Proving Termination of Programs Automatically with AProVE. | Jrgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plcker, Peter Schneider-Kamp, Thomas Strder, Stephanie Swiderski, Ren Thiemann |
| 2014 | CADE | Proving Termination and Memory Safety for Programs with Pointer Arithmetic. | Thomas Strder, Jrgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp |
| 2014 | TACAS | Alternating Runtime and Size Complexity Analysis of Integer Programs. | Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jrgen Giesl |
| 2012 | CADE | Exotic Semi-Ring Constraints. | Michael Codish, Yoav Fekete, Carsten Fuhs, Jrgen Giesl, Johannes Waldmann |
| 2012 | CADE | Proving Non-looping Non-termination Automatically. | Fabian Emmes, Tim Enger, Jrgen Giesl |
| 2012 | CAV | Automated Termination Proofs for Java Programs with Cyclic Data. | Marc Brockschmidt, Richard Musiol, Carsten Otto, Jrgen Giesl |
| 2012 | LOPSTR | Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. | Jrgen Giesl, Thomas Strder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs |
| 2012 | PPDP | Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. | Jrgen Giesl, Thomas Strder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs |
| 2011 | CADE | A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. | Lars Noschinski, Fabian Emmes, Jrgen Giesl |
| 2011 | ITP | Termination of Isabelle Functions via Termination of Rewriting. | Alexander Krauss, Christian Sternagel, Ren Thiemann, Carsten Fuhs, Jrgen Giesl |
| 2011 | LOPSTR | A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. | Thomas Strder, Fabian Emmes, Peter Schneider-Kamp, Jrgen Giesl, Carsten Fuhs |
| 2010 | LOPSTR | Dependency Triples for Improving Termination Analysis of Logic Programs with Cut. | Thomas Strder, Peter Schneider-Kamp, Jrgen Giesl |
| 2010 | LPAR | Lazy Abstraction for Size-Change Termination. | Michael Codish, Carsten Fuhs, Jrgen Giesl, Peter Schneider-Kamp |
| 2009 | CADE | Termination Analysis by Dependency Pairs and Inductive Theorem Proving. | Stephan Swiderski, Michael Parting, Jrgen Giesl, Carsten Fuhs, Peter Schneider-Kamp |
| 2009 | LOPSTR | The Dependency Triple Framework for Termination of Logic Programs. | Peter Schneider-Kamp, Jrgen Giesl, Manh Thang Nguyen |
| 2008 | AISC | Search Techniques for Rational Polynomial Orders. | Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jrgen Giesl, Salvador Lucas, Peter Schneider-Kamp |
| 2008 | LPAR | Improving Context-Sensitive Dependency Pairs. | Beatriz Alarcn, Fabian Emmes, Carsten Fuhs, Jrgen Giesl, Ral Gutirrez, Salvador Lucas, Peter Schneider-Kamp, Ren Thiemann |
| 2007 | CADE | Proving Termination by Bounded Increase. | Jrgen Giesl, Ren Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
| 2007 | LOPSTR | Termination Analysis of Logic Programs Based on Dependency Graphs. | Manh Thang Nguyen, Jrgen Giesl, Peter Schneider-Kamp, Danny De Schreye |
| 2007 | SAT | SAT Solving for Termination Analysis with Polynomial Interpretations. | Carsten Fuhs, Jrgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren Thiemann, Harald Zankl |
| 2006 | CADE | Automatic Termination Proofs in the Dependency Pair Framework. | Jrgen Giesl, Peter Schneider-Kamp, Ren Thiemann |
| 2006 | LOPSTR | Automated Termination Analysis for Logic Programs by Term Rewriting. | Peter Schneider-Kamp, Jrgen Giesl, Alexander Serebrenik, Ren Thiemann |
| 2006 | LPAR | SAT Solving for Argument Filterings. | Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, Ren Thiemann, Jrgen Giesl |
| 2004 | CADE | Improved Modular Termination Proofs Using Dependency Pairs. | Ren Thiemann, Jrgen Giesl, Peter Schneider-Kamp |
| 2004 | LPAR | The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp |
| 2003 | CADE | Deciding Inductive Validity of Equations. | Jrgen Giesl, Deepak Kapur |
| 2003 | LPAR | Improving Dependency Pairs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp, Stephan Falke |
| 2002 | DLT | Innermost Termination of Context-Sensitive Rewriting. | Jrgen Giesl, Aart Middeldorp |
| 2001 | CADE | Decidable Classes of Inductive Theorems. | Jrgen Giesl, Deepak Kapur |
| 2000 | CADE | Eliminating Dummy Elimination. | Jrgen Giesl, Aart Middeldorp |
| 2000 | CSL | Equational Termination by Semantic Labelling. | Hitoshi Ohsaki, Aart Middeldorp, Jrgen Giesl |
| 1999 | CSL | Applying Rewriting Techniques to the Verification of Erlang Processes. | Thomas Arts, Jrgen Giesl |
| 1999 | LOPSTR | Context-Moving Transformations for Function Verification. | Jrgen Giesl |
| 1998 | CADE | Termination Analysis by Inductive Evaluation. | Jrgen Brauburger, Jrgen Giesl |
| 1996 | SAS | Termination Analysis for Partial Functions. | Jrgen Brauburger, Jrgen Giesl |
| 1995 | KI | Automated Termination Proofs with Measure Functions. | Jrgen Giesl |
| 1995 | SAS | Termination Analysis for Functional Programs using Term Orderings | Jrgen Giesl |
| 1994 | KI | Strategies for Semantical Contractions. | Jrgen Giesl, Ingrid Neumann |
| 1993 | EPIA | The Semantics of Rational Contractions. | Jrgen Giesl, Ingrid Neumann |