Walther, Christoph (2019):
Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base.
In: ACM Transactions on Mathematical Software (TOMS), 45 (1), pp. 9⋅1-9⋅7. DOI: 10.1145/3301317,
[Article]

Walther, Christoph (2018):
A Machine Assisted Proof of the Chinese Remainder Theorem.
In: VeriFun Reports, Darmstadt, Technische Universität, VFR 18/03, [Report]

Walther, Christoph (2018):
Formally Verified Montgomery Multiplication.
pp. 505-522, 30th Intern. Conf. on Computer Aided Verification (CAV 2018), Oxford, UK, 14.-17.07., ISBN 978-3-319-96142-2,
DOI: 10.1007/978-3-319-96142-2_30,
[Conference or Workshop Item]

Walther, Christoph ; Wasser, Nathan (2017):
Fermat, Euler, Wilson - Three Case Studies in Number Theory.
In: Journal of Automated Reasoning, 59 (2), pp. 267-286. Springer, ISSN 1573-0670,
DOI: 10.1007/s10817-016-9387-z,
[Article]

Anikeev, Maxim ; Madlener, Felix ; Schlosser, Andreas ; Huss, Sorin ; Walther, Christoph (2010):
Viable Approach to Machine-Checked Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography.
pp. 95-101, Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010), Kazan, Russia, June 14-15, 2010, [Conference or Workshop Item]

Schlosser, A. ; Walther, Christoph ; Gonder, M. ; Aderhold, Markus (2007):
Context dependent procedures and computed types in veriFun.
In: Electronic Notes in Theoretical Computer Science, 174 (7), pp. 61-78. ISSN 1571-0661,
DOI: 10.1016/j.entcs.2006.10.038,
[Article]

Anikeev, Maxim ; Madlener, Felix ; Schlosser, Andreas ; Huss, Sorin A. ; Walther, Christoph (2007):
Automated Verification for an Efficient Elliptic-Curve Algorithm - A Case Study.
Information Security: Proceedings of the IX. International Conference, January 2007, [Conference or Workshop Item]

Walther, Christoph (2006):
A Pragmatic Approach to Equality Reasoning.
In: VeriFun Reports, Darmstadt, Technische Universität, VFR 06/02, [Report]

Schlosser, Andreas ; Walther, Christoph ; Aderhold, Markus (2006):
Axiomatic specification in VeriFun.
pp. 146-163, IJCAR’06-Workshop Verification Workshop (VERIFY-06), Seattle, USA, August 2006, [Conference or Workshop Item]

Schlosser, Andreas ; Walther, Christoph ; Gonder, Michael ; Aderhold, Markus (2006):
Context Dependent Procedures and Computed Types in VeriFun.
IJCAR 2006-Workshop Programming Languages meets Program Verification (PLPV 2006), Seattle, USA, 21.08.2006, [Conference or Workshop Item]

Aderhold, Markus ; Walther, Christoph ; Szallies, Daniel ; Schlosser, Andreas (2006):
A Fast Disprover for VeriFun.
pp. 59-69, IJCAR’06-Workshop DISPROVING’06: Non-Theorems, Non-Validity ,Non-Provability, Seattle, USA, 10. - 22.08.2006, [Conference or Workshop Item]

Walther, Christoph ; Aderhold, Markus ; Schlosser, Andreas (2006):
The L 1.0 Primer.
VFR06/01, TU Darmstadt, [Report]

Walther, Christoph ; Schweitzer, Stephan (2005):
Automated termination analysis for incompletely defined programs.
pp. 332-346, 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004), Montevideo, Uruguay, 14.-18.03.2005, [Conference or Workshop Item]

Walther, Christoph ; Schweitzer, Stephan (2005):
Reasoning about incompletely defined programs.
pp. 427-442, 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2005), Montego Bay, Jamaica, 02.-06.12., ISSN 978-3-540-30553-8,
DOI: 10.1007/11591191_30,
[Conference or Workshop Item]

Walther, Christoph ; Schweitzer, Stephan (2004):
Verification in the classroom.
In: Journal of Automated Reasoning, 32 (1), pp. 35-73. ISSN 0168-7433,
DOI: 10.1023/B:JARS.0000021872.64036.41,
[Article]

Walther, Christoph ; Schweitzer, Stephan (2003):
About VeriFun.
pp. 322-327, 19th International Conference on Automated Deduction (CADE-19), Miami Beach, USA, 28.07.-02.08.2003, DOI: 10.1007/978-3-540-45085-6_28,
[Conference or Workshop Item]

Walther, Christoph ; Schweitzer, Stephan (2003):
A Machine-Verified Code Generator.
pp. 91-106, 10th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-10), Almaty, Kazakhstan, 22.-26. Sept., 2003, ISBN 978-3-540-20101-4,
DOI: 10.1007/978-3-540-39813-4_6,
[Conference or Workshop Item]

Walther, Christoph ; Schweitzer, Stephan (2002):
VeriFun user guide.
Darmstadt, Techn. Univ., Fachgebiet Programmiermethodik, VFR 02/01, [Report]

Walther, Christoph ; Schweitzer, Stephan (2002):
The VeriFun tutorial.
Darmstadt, Techn. Univ., Fachgebiet Programmiermethodik, VFR 02/04, [Report]

Walther, Christoph ; Schweitzer, Stephan (2002):
A machine supported proof of the unique prime factorization theorem.
Darmstadt, Techn. Univ., Fachgebiet Programmiermethodik, VFR 02/03, [Report]

Walther, Christoph ; Schweitzer, Stephan (2002):
A verification of binary search.
Darmstadt, Techn. Univ., Fachgebiet Programmiermethodik, VFR 02/02, [Report]

Walther, Christoph (2002):
Programmiermethodik.
In: 30 Jahre Informatik an deutschen Hochschulen, p. 100, Darmstadt, Techn. Univ., [Book Section]

Walther, Christoph (2001):
Semantik und Programmverifikation.
In: Teubner-Texte zur Informatik, 1. Auflage, Stuttgart [u.a.], Teubner, ISBN 978-3-322-86768-1,
[Book]

Walther, Christoph ; Kolbe, Thomas (2000):
On terminating lemma speculations.
In: Information and computation, 162 (1-2), pp. 96-116. ISSN 0890-5401,
DOI: 10.1006/inco.1999.2859,
[Article]

Walther, Christoph ; Kolbe, Thomas (2000):
Proving theorems by reuse.
In: Artificial Intelligence, 116 (1-2), pp. 17-66. Elsevier, ISSN 0004-3702,
DOI: 10.1016/S0004-3702(99)00096-X,
[Article]

Walther, Christoph
Hölldobler, S. (ed.) (2000):
Criteria for termination.
In: Intellectics and computational logic: Papers in honor of Wolfgang Bibel, pp. 361-386, Dordrecht (u.a.), Kluwer Academic, DOI: 10.1007/978-94-015-9383-0,
[Book Section]

Kolbe, Thomas ; Walther, Christoph
Bibel, Wolfgang (ed.) (1998):
Proof Analysis, Generalization and Reuse.
10, In: Automated deduction: a basis for applications. Bd.2, pp. 189-219, Dordrecht, Kluwer Acad. Publ, DOI: 10.1007/978-94-017-0435-9,
[Book Section]

Giesl, Jürgen ; Walther, Christoph ; Brauburger, J.
Bibel, Wolfgang (ed.) (1998):
Termination Analysis for Functional Programs.
10, In: Automated deduction: a basis for applications. Bd. 3, pp. 135-164, Dordrecht, Kluwer Acad. Publ, DOI: 10.1007/978-94-017-0437-3,
[Book Section]

Kolbe, Thomas ; Walther, Christoph (1996):
Proving theorems by mimicking a human's skill.
pp. 50-56, The 1996 AAAI Spring Symposium, Palo Alto, USA, 25.–27.03, [Conference or Workshop Item]

Kolbe, Thomas ; Walther, Christoph (1996):
Termination of theorem proving by reuse.
pp. 106-120, 13th International Conference on Automated Deduction (CADE-13), New Brunswick, USA, 30.07.-03.08.1996, DOI: 10.1007/3-540-61511-3_72,
[Conference or Workshop Item]

Walther, Christoph
Görz, Günther (ed.) (1995):
Automatisches Beweisen.
In: Einführung in die Künstliche Intelligenz, 2. Aufl, pp. 203-241, Bonn, Addison-Wesley, [Book Section]

Kolbe, Thomas ; Walther, Christoph (1995):
Adaption of Proofs for Reuse.
1995 Fall Symposium Adaptation of Knowledge for Reuse, Cambridge, USA, 10.-12.11., [Conference or Workshop Item]

Kolbe, Thomas ; Walther, Christoph (1995):
Patching proofs for reuse.
pp. 303-306, ECML'95: 8th European Conference on Machine Learning, Heraclion, Greece, 25. - 27.04., [Conference or Workshop Item]

Kolbe, Thomas ; Walther, Christoph (1995):
Proof management and retrieval.
14th International Joint Conference on Artificial Intelligence - Workshop for Formal Approaches to the Reuse of Plans, Proofs and Programs, Montreal, Canada, 20.-25.08.1995, [Conference or Workshop Item]

Kolbe, Thomas ; Walther, Christoph (1995):
Second-Order Matching modulo Evaluation: A technique for Reusing Proofs.
pp. 190-195, IJCAI '95: 14th International Joint Conference on Artificial Intelligence, Montreal, Canada, 20.-25.08.1995, [Conference or Workshop Item]

Walther, Christoph (1994):
On Proving the Termination of Algorithms by Machine.
In: Artificial Intelligence, 71 (1), pp. 101-157. Elsevier, DOI: 10.1016/0004-3702(94)90063-9,
[Article]

Kolbe, Thomas ; Walther, Christoph (1994):
Reusing Proofs.
pp. 80-84, ECAI'94: 11th European Conference on Artificial Intelligence, Amsterdam, Netherlands, 08.-12.08., [Conference or Workshop Item]

Walther, Christoph
Gabbay, D. M. ; Hogger, C. J. ; Robinson, J. A. (eds.) (1994):
Mathematical Induction.
2, In: Handbook of Logic in Artificial Intelligence and Logic Programming - Volume 2: Deduction Methodologies, pp. 127-228, Oxford, Oxford University Press, ISBN 9780198537465,
[Book Section]

Walther, Christoph
Bajcsy, Ruzena (ed.) (1993):
Combining Induction Axioms by Machine.
pp. 95-101, Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-13), Chambery, France, 28.08.- 03.09.1993, ISBN 1-55860-300-X,
[Conference or Workshop Item]

Walther, Christoph
Voronkov, Andrei (ed.) (1992):
Computing Induction Axioms.
pp. 381-392, Springer, Proc. of the Inter. Conf. on Logic Programming and Automated Reasoning (LPAR-1992), St. Petersburg, Russia, 15.-20.07.1992, ISSN 978-3-540-55727-2, e-ISSN 978-3-540-47279-7,
DOI: 10.1007/BFb0013076,
[Conference or Workshop Item]

Walther, Christoph
Shapiro, Stuart S. (ed.) (1992):
Mathematical Induction.
In: Encyclopedia of Artificial Intelligence-Volume 2, pp. 668-672, New York, John Wiley and Sons, ISBN 978-0-471-50305-7,
[Book Section]