Christoph Walther

Prof. Dr. Christoph Walther

Hochschulstraße 10
64289 Darmstadt

Raum: S2|02 A309

+49 6151 16-4492
+49 6151 16-6241
+49 175 5503218


zur Liste

Sprechstunde: nach Vereinbarung

Research Interests

Formal Methods, Automated Reasoning, Theorem Proving, Semantics and Verification, Machine Learning, Formal Methods in Education. Presently involved with the development of the verification tool VeriFun.

Teaching

Selected Publications

[Schlosser et al.(2007) Schlosser, Walther, Gonder, and Aderhold]
Andreas Schlosser, Christoph Walther, Michael Gonder, and Markus Aderhold.
Context Dependent Procedures and Computed Types in VeriFun. Electronic Notes in Theoretical Computer Science, 174(7):61-78, 2007. pdf
[Aderhold et al.(2006) Aderhold, Walther, Szallies, and Schlosser]
Markus Aderhold, Christoph Walther, Daniel Szallies, and Andreas Schlosser.
A Fast Disprover for VeriFun. In Wolfgang Ahrendt, Peter Baumgartner, and Hans de Nivelle, editors, Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06), pages 59-69, Seattle, WA, 2006. Federated Logic Conference. pdf
[Andreas Schlosser et al.(2006) Schlosser, Walther, and Aderhold]
Andreas Schlosser, Christoph Walther, and Markus Aderhold.
Axiomatic Specifications in VeriFun. In Serge Autexier and Heiko Mantel, editors, Proc. 6th Verification Workshop (VERIFY-06), pages 146-163, Seattle, WA, 2006. Federated Logic Conference. pdf
[Walther and Schweitzer(2006)]
Christoph Walther and Stephan Schweitzer.
A Pragmatic Approach to Equality Reasoning. Technical Report VFR 06/02, Programmiermethodik, Technische Universität Darmstadt, 2006. pdf
[Walther et al.(2006)Walther, Aderhold, and Schlosser]
Christoph Walther, Markus Aderhold, and Andreas Schlosser.
The L 1.0 Primer. Technical Report VFR 06/01, Programmiermethodik, Technische Universität Darmstadt, 2006. pdf
[Walther and Schweitzer(2005b)]
Christoph Walther and Stephan Schweitzer.
Reasoning about Incompletely Defined Programs. In Geoff Sutcliffe and Andrei Voronkov, editors, Proc. of the 12th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-12), volume 3835 of Lecture Notes in Artificial Intelligence, pages 427—442, Montego Bay, Jamaica, 2005b. Springer. pdf
[Walther and Schweitzer(2005a)]
Christoph Walther and Stephan Schweitzer.
Automated Termination Analysis for Incompletely Defined Programs. In Franz Baader and Andrei Voronkov, editors, Proc. of the 11th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-11), volume 3452 of Lecture Notes in Artifical Intelligence, pages 332—346, Montevideo, Uruguay, 2005, Springer-Verlag. pdf
[Walther and Schweitzer(2004d)]
Christoph Walther and Stephan Schweitzer.
Automated Termination Analysis for Incompletely Defined Programs. Technical Report VFR 04/03, Programmiermethodik, Technische Universität Darmstadt, 2004.
[Walther and Schweitzer(2004c)]
Christoph Walther and Stephan Schweitzer.
Reasoning about Incompletely Defined Programs. Technical Report VFR 04/02, Programmiermethodik, Technische Universität Darmstadt, 2004.
[Walther(2004b)]
Christoph Walther.
Improvements of the Estimation Calculus. Technical Report VFR 04/01, Programmiermethodik, Technische Universität Darmstadt, 2004.
[Walther and Schweitzer(2004a)]
Christoph Walther and Stephan Schweitzer.
Verification in the Classroom. Journal of Automated Reasoning – Special Issue on Automated Reasoning and Theorem Proving in Education, 32(1):35-73, 2004a. pdf
[Walther(2003)]
Christoph Walther.
Automatisches Beweisen. In G. Görz, editor, Einführung in die Künstliche Intelligenz. Oldenbourg,München, 4th edition, 2003.
[Walther and Schweitzer(2003c)]
Christoph Walther and Stephan Schweitzer.
A Machine-Verified Code Generator. In Moshe Y. Vardi and Andrei Voronkov, editors, Proc. of the 10th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-10), volume 2850 of Lecture Notes in Artifical Intelligence, pages 91—106, Almaty, Kazakhstan, 2003c. Springer-Verlag. pdf
[Walther and Schweitzer(2003b)]
Christoph Walther and Stephan Schweitzer.
About VeriFun . In Franz Baader, editor, Proc. of the 19th Inter. Conf. on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Artifical Intelligence, pages 322—327, Miami Beach, 2003b. Springer-Verlag. pdf
[Walther(2003)]
Christoph Walther.
Concept Formation. In Simon Colton, Jeremy Gow, Volker Sorge, and Toby Walsh, editors, Proc. of the CADE-19 Workshop on Challenges and Novel Applications for Automated Reasoning, pages 25-32, Miami Beach, 2003.
[Walther and Schweitzer(2003a)]
Christoph Walther and Stephan Schweitzer.
A Machine-Verified Code Generator. Technical Report VFR 03/01, Programmiermethodik, Technische Universität Darmstadt, 2003a. pdf
[Walther and Schweitzer(2002d)]
Christoph Walther and Stephan Schweitzer.
The VeriFun Tutorial. Technical Report VFR 02/04, Programmiermethodik, Technische Universität Darmstadt, 2002d. pdf
[Walther and Schweitzer(2002f)]
Christoph Walther and Stephan Schweitzer.
A Machine Supported Proof of the Unique Prime Factorization Theorem. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, Proc. of the 5th Workshop on Tools for System Design and Verification (FM-TOOLS 2002), volume 2002-11 of Report, Institut für Informatik, Universität Augsburg, pages 39-45, Augsburg, 2002f.
[Walther and Schweitzer(2002c)]
Christoph Walther and Stephan Schweitzer.
A Machine Supported Proof of the Unique Prime Factorization Theorem. Technical Report VFR 02/03, Programmiermethodik, Technische Universität Darmstadt, 2002c. pdf
[Walther and Schweitzer(2002b)]
Christoph Walther and Stephan Schweitzer.
A Verification of Binary Search. Technical Report VFR 02/02, Programmiermethodik, Technische Universität Darmstadt, 2002b. pdf
[Walther and Schweitzer(2002a)]
Christoph Walther and Stephan Schweitzer.
VeriFun User Guide. Technical Report VFR 02/01, Programmiermethodik, Technische Universität Darmstadt, 2002a. pdf
[Walther(2001)]
Christoph Walther.
Semantik und Programmverifikation. Teubner-Wiley, Leipzig, 2001. pdf
[Walther(2000)]
Christoph Walther.
Criteria for Termination. In S. Hölldobler, editor, Intellectics and Computational Logic, pages 361—386. Kluwer Academic Publishers, Dordrecht, 2000. ps
[Walther and Kolbe(2000b)]
Christoph Walther and Thomas Kolbe.
On Terminating Lemma Speculations. Information and Computation, 162:96—116, 2000b. pdf
[Walther and Kolbe(2000a)]
ChristophWalther and Thomas Kolbe.
Proving theorems by reuse. Artificial Intelligence, 116:17—66, 2000a. pdf
[Kolbe and Walther(1998)]
Thomas Kolbe and Christoph Walther.
Proof Analysis, Generalization and Reuse. In W. Bibel and P. Schmitt, editors, Automated Deduction – A Basis for Applications, volume 2, pages 189—219. Kluwer Academic Publishers, Dordrecht, 1998. ps
[Giesl et al.(1998)Giesl, Walther, and Brauburger]
Jürgen Giesl, Christoph Walther, and Jürgen Brauburger.
Termination Analysis for Functional Programs. In W. Bibel and P. Schmitt, editors, Automated Deduction – A Basis for Applications, volume 3, pages 135—164. Kluwer Academic Publishers, Dordrecht, 1998. ps
[Kolbe and Walther(1996b)]
Thomas Kolbe and Christoph Walther.
Termination of Theorem Proving by Reuse. In M. A. McRobbie and J. K. Slaney, editors, Proc. of the 13th Inter. Conf. on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artifical Intelligence, pages 106— 120, New Brunswick, NJ, 1996b. Springer-Verlag. pdf ps
[Kolbe and Walther(1996a)]
Thomas Kolbe and Christoph Walther.
Proving Theorems by Mimicking a Human’s Skill. In Proc. AAAI 1996 Spring Symposium on Acquisition, Learning and Demonstration, pages 50—56, Stanford, CA, 1996a. The AAAI Press. ps
[Kolbe and Walther(1995d)]
Thomas Kolbe and Christoph Walther.
Adaption of Proofs for Reuse. In Proc. AAAI 1995 Fall Symposium on Adaption of Knowledge for Reuse, pages 61—67, Cambridge, MA, 1995d. The AAAI Press. ps
[Kolbe and Walther(1995c)]
Thomas Kolbe and Christoph Walther.
Proof Management and Retrieval. In Proc. IJCAI- 14 Workshop on Formal Approaches to the Reuse of Plans, Proofs and Programs, Montreal, Canada, 1995c. ps
[Kolbe and Walther(1995b)]
Thomas Kolbe and Christoph Walther.
Second-Order Matching modulo Evaluation – A Technique for Reusing Proofs. In Proc. 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14), pages 190— 195, Montreal, Canada, 1995b. Morgan Kaufmann. pdf
[Kolbe and Walther(1995a)]
Thomas Kolbe and Christoph Walther.
Patching Proofs for Reuse. In Proc. of the 8th European Conf. on Machine Learning (ECML-8), volume 912 of Lecture Notes in Artifical Intelligence, pages 303— 306, Heraklion, Crete, 1995a. Springer-Verlag. pdf
[Kolbe and Walther(1994)]
Thomas Kolbe and Christoph Walther.
Reusing Proofs. In Proc. of the 11th European Conf. on Artificial Intelligence (ECAI-11), pages 80—84, Amsterdam, 1994. pdf ps
[Walther(1994b)]
Christoph Walther.
On Proving the Termination of Algorithms by Machine. Artificial Intelligence, 71(1):101—157, 1994b. pdf
[Walther(1994a)]
Christoph Walther.
Mathematical Induction. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 127—227. Oxford University Press, Oxford, 1994a. pdf
[Walther(1993)]
Christoph Walther.
Combining Induction Axioms by Machine. In Ruzena Bajcsy, editor, Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-13), pages 95-101, Chambery, France, 1993. Morgan Kaufmann. pdf
[Walther(1992b)]
Christoph Walther.
Computing Induction Axioms. In Andrei Voronkov, editor, Proc. of the Inter. Conf. on Logic Programming and Automated Reasoning (LPAR-1992), volume 624 of Lecture Notes in Artifical Intelligence, pages 381—392, St. Petersburg, Russia, 1992b. Springer-Verlag. pdf
[Walther(1992a)]
Christoph Walther.
Mathematical Induction. In S. C. Shapiro, editor, Encyclopedia of Artificial Intelligence, pages 668—672. John Wiley and Sons, New York, 1992a.
[Walther(1991)]
Christoph Walther.
Automatisierung von Terminierungsbeweisen. Vieweg, Braunschweig, 1991.
[Walther(1990)]
Christoph Walther.
Many-Sorted Inferences in Automated Theorem Proving. In K.-H. Bläsius, U. Hedtstück, and C.-R. Rollinger, editors, Sorts and Types in Artificial Intelligence, volume 418 of Lecture Notes in Ariticial Intelligence, pages 18-48, Springer- Verlag, 1990.
[Walther(1989)]
Christoph Walther.
Many-Sorted Resolution. In Th. Christaller, editor, Künstliche Intelligenz – 5. Frühjahrsschule, KIFS-87, volume 202 of Fachberichte Informatik, pages 65-102, Springer-Verlag, 1989.
[Walther(1988d)]
Christoph Walther.
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. In Proc. of the 9th Inter. Conf. on Automated Deduction (CADE-9), volume 310 of Lecture Notes in Artifical Intelligence, pages 602-621, Argonne, IL, 1988d. Springer-Verlag.
[Walther(1988c)]
Christoph Walther.
Automatisches Beweisen. In Th. Christaller, H.- W. Hein, and M. M. Richter, editors, Künstliche Intelligenz – Theoretische Grundlagen und Anwendungsfelder, volume 159 of Fachberichte Informatik, pages 292-339, Springer-Verlag, 1988c.
[Walther(1988b)]
Christoph Walther.
An obvious Solution for a non-obvious Problem. Newsletter of the Association for Automated Reasoning (AAR), no 9, 1988b.
[Walther(1988a)]
Christoph Walther.
Many-Sorted Unification. J. ACM, 35(1):1—17, 1988a. pdf
[Walther(1987)]
ChristophWalther.
A Many-Sorted Calculus Based on Resolution and Paramodulation. Pitman and Morgan Kaufmann, London and Los Altos, 1987.
[Walther(1986)]
ChristophWalther.
A Classification of Many-Sorted Unification Problems. In J. H. Siekmann, editor, Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8), volume 230 of Lecture Notes in Artifical Intelligence, pages 525—537, Oxford, UK, 1986. Springer- Verlag.
[Biundo et al.(1986)Biundo, Hummel, Hutter, and Walther]
Susanne Biundo, Birgit Hummel, Dieter Hutter, and Christoph Walther.
The Karlsruhe Induction Theorem Proving System. In J. H. Siekmann, editor, Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8), volume 230 of Lecture Notes in Artifical Intelligence, pages 672— 674, Oxford, UK, 1986. Springer-Verlag.
[Walther(1985)]
Christoph Walther.
A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution. Artificial Intelligence, 26(2):217-224, 1985. pdf
[Walther(1984b)]
Christoph Walther.
Unification in Many- Sorted Theories. In Tim O’Shea, editor, Advances in Artificial Intelligence – Proc. of the 6th European Conf. on Artificial Intelligence (ECAI-6), pages 383-392, Pisa, 1984b. North- Holland.
[Walther(1984a)]
Christoph Walther.
A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution. In Proc. of the 4th National Conf. on Artificial Intelligence (AAAI-4), pages 330-334, Austin, TX, 1984a. Morgan Kaufmann.
[Walther(1983)]
Christoph Walther.
A Many-Sorted Calculus based on Resolution and Paramodulation. In Alan Bundy, editor, Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8), pages 882-891, Karlsruhe, Germany, 1983. Morgan Kaufmann.
[Walther(1981)]
Christoph Walther.
Elimination of Redundant Links in Extended Connection Graphs. In Tagungsband der 8. GI-Fachtagung für Künstliche Intelligenz (GWAI-8), volume 47 of Fachberichte Informatik, pages 201-213, Bad Honnef, 1981. Springer- Verlag.
[Bläsius et al.(1981)Bläsius, Eisinger, Herold, Siekmann, Smolka, and Walther]
Karl Bläsius, Norbert Eisinger, Alexander Herold, Jörg Siekmann, Gerd Smolka, and Christoph Walther.
The Markgraf Karl Refutation Procedure (Fall 1981). In Proc. of the 7th Intern. Joint Conf. on Artificial Intelligence (IJCAI-7), pages 511-518, Vancouver, Canada, 1981. Morgan Kaufmann.
[Eisinger et al.(1980b)Eisinger, Siekmann, Smolka, Unvericht, and Walther]
Norbert Eisinger, Jörg Siekmann, Gerd Smolka, Eva Unvericht, and Christoph Walther.
Das Karlsruher Beweissystem. In Tagungsband der 10. GI-Jahrestagung, volume 33 of Fachberichte Informatik, pages 400-412, Saarbrücken, 1980b. Springer-Verlag.
[Eisinger et al.(1980a)Eisinger, Siekmann, Smolka, Unvericht, and Walther]
Norbert Eisinger, Jörg Siekmann, Gerd Smolka, Eva Unvericht, and Christoph Walther.
The Markgraf Karl Refutation Procedure. In Proc. of the AISB Conf. on Artificial Intelligence, Amsterdam, 1980a.
[Kammerer and Walther(1976)]
Peter Kammerer and Christoph Walther.
Device Monitors. In Proc. of the 1976 IFAC/IFIP Workshop on Real-Time Programming, Rocquencourt, France, 1976.