| 2018 | CAV | Formally Verified Montgomery Multiplication. | Christoph Walther |
| 2005 | LPAR | Reasoning About Incompletely Defined Programs. | Christoph Walther, Stephan Schweitzer |
| 2004 | LPAR | Automated Termination Analysis for Incompletely Defined Programs. | Christoph Walther, Stephan Schweitzer |
| 2003 | CADE | About VeriFun. | Christoph Walther, Stephan Schweitzer |
| 2003 | LPAR | A Machine-Verified Code Generator. | Christoph Walther, Stephan Schweitzer |
| 1996 | CADE | Termination of Theorem Proving by Reuse. | Thomas Kolbe, Christoph Walther |
| 1995 | IJCAI | Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs. | Thomas Kolbe, Christoph Walther |
| 1994 | ECAI | Reusing Proofs. | Thomas Kolbe, Christoph Walther |
| 1993 | IJCAI | Combining Induction Axioms by Machine. | Christoph Walther |
| 1992 | LPAR | Computing Induction Axioms. | Christoph Walther |
| 1988 | CADE | Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. | Christoph Walther |
| 1987 | KI | Many-Sorted Resolution. | Christoph Walther |
| 1986 | CADE | The Karlsruhe Induction Theorem Proving System. | Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther |
| 1986 | CADE | A Classification of Many-Sorted Unification Problems. | Christoph Walther |
| 1986 | KI | Automatisches Beweisen. | Christoph Walther |
| 1984 | AAAI | A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution. | Christoph Walther |
| 1984 | ECAI | Unification in Many-Sorted Theories. | Christoph Walther |
| 1983 | IJCAI | A Many-Sorted Calculus Based on Resolution and Paramodulation. | Christoph Walther |
| 1981 | IJCAI | The Markgraf Karl Refutation Procedure. | Karl-Hans Blsius, Norbert Eisinger, Jrg H. Siekmann, Gert Smolka, Alexander Herold, Christoph Walther |
| 1981 | KI | Elimination of Redundant Links in Extended Connection Graphs. | Christoph Walther |
| 1980 | GI | Das Karlsruher Beweissystem. | Norbert Eisinger, Jrg H. Siekmann, Gert Smolka, E. Unvericht, Christoph Walther |