| 2014 | TACAS | Alternating Runtime and Size Complexity Analysis of Integer Programs. | Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jrgen Giesl |
| 2013 | TACAS | LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution). | Stephan Falke, Florian Merz, Carsten Sinz |
| 2012 | CADE | Rewriting Induction + Linear Arithmetic = Decision Procedure. | Stephan Falke, Deepak Kapur |
| 2012 | CADE | A Theory of Arrays with set and copy Operations. | Stephan Falke, Carsten Sinz, Florian Merz |
| 2012 | CADE | Challenges in Comparing Software Verification Tools for C. | Florian Merz, Carsten Sinz, Stephan Falke |
| 2012 | TACAS | LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). | Carsten Sinz, Florian Merz, Stephan Falke |
| 2009 | CADE | A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. | Stephan Falke, Deepak Kapur |
| 2007 | CADE | Dependency Pairs for Rewriting with Non-free Constructors. | Stephan Falke, Deepak Kapur |
| 2006 | LPAR | Inductive Decidability Using Implicit Induction. | Stephan Falke, Deepak Kapur |
| 2003 | LPAR | Improving Dependency Pairs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp, Stephan Falke |