| 2026 | IJCAR | Accelerating Loops with Arrays. | Florian Frohn, 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 |
| 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 | IJCAR | Satisfiability Modulo Exponential Integer Arithmetic. | Florian Frohn, Jrgen Giesl |
| 2023 | CADE | Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). | Florian Frohn, 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 |
| 2020 | LPAR | Polynomial Loops: Beyond Termination. | Marcel Hark, Florian Frohn, Jrgen Giesl |
| 2020 | SAS | Termination of Polynomial Loops. | Florian Frohn, Marcel Hark, Jrgen Giesl |
| 2020 | TACAS | A Calculus for Modular Loop Acceleration. | Florian Frohn |
| 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 |
| 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 | 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 |