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

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

Inductive Decidability Using Implicit Induction. - Stephan Falke 001; Deepak Kapur (LPAR, 2006)

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

Dependency Pairs for Rewriting with Non-free Constructors. - Stephan Falke 001; Deepak Kapur (CADE, 2007)

Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures. - Stephan Falke 001; Deepak Kapur (RTA, 2008)

Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures. - Stephan Falke 001; Deepak Kapur (WRS@RTA, 2008)

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. - Stephan Falke 001; Deepak Kapur (CADE, 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)

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

Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures. - Stephan Falke 001; Deepak Kapur (WFLP, 2009)

A Precise Memory Model for Low-Level Bounded Model Checking. - Carsten Sinz; Stephan Falke 001; Florian Merz 001 (SSV, 2010)

Termination Analysis of C Programs Using Compiler Intermediate Languages. - Stephan Falke 001; Deepak Kapur; Carsten Sinz (RTA, 2011)

Rewriting Induction + Linear Arithmetic = Decision Procedure. - Stephan Falke 001; Deepak Kapur (IJCAR, 2012)

A Theory of Arrays with set and copy Operations. - Stephan Falke 001; Carsten Sinz; Florian Merz 001 (SMT@IJCAR, 2012)

Challenges in Comparing Software Verification Tools for C. - Florian Merz 001; Carsten Sinz; Stephan Falke 001 (COMPARE, 2012)

LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). - Carsten Sinz; Florian Merz 001; Stephan Falke 001 (TACAS, 2012)

Termination Analysis of Imperative Programs Using Bitvector Arithmetic. - Stephan Falke 001; Deepak Kapur; Carsten Sinz (VSTTE, 2012)

LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. - Florian Merz 001; Stephan Falke 001; Carsten Sinz (VSTTE, 2012)

Review of introduction to mathematics of satisfiability, by Victor W. Marek. - Stephan Falke 001 (SIGACT News, 2012)

Review of transitions and trees: an introduction to structural operational semantics, by Hans Hüttel. - Stephan Falke 001 (SIGACT News, 2012)

The bounded model checker LLBMC. - Stephan Falke 001; Florian Merz 001; Carsten Sinz (ASE, 2013)

LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution). - Stephan Falke 001; Florian Merz 001; Carsten Sinz (TACAS, 2013)

Extending the Theory of Arrays: memset, memcpy, and Beyond. - Stephan Falke 001; Florian Merz 001; Carsten Sinz (VSTTE, 2013)

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

When Is a Formula a Loop Invariant? - Stephan Falke 001; Deepak Kapur (Logic, Rewriting, and Concurrency, 2015)

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)