| 2023 | CADE | Proving Termination of C Programs with Lists. | Jera Hensel, Jrgen Giesl |
| 2022 | TACAS | AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution). | Jera Hensel, Constantin Mensendiek, 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 and Memory Safety for Programs with Pointer Arithmetic. | Thomas Strder, Jrgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp |