A

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.
Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010). Kazan, Russia (14.06.2010-15.06.2010)
Konferenzveröffentlichung, Bibliographie

Aderhold, Markus Axel (2009)
Verification of second-order functional programs.
Technische Universität Darmstadt
Dissertation, Bibliographie

Aderhold, Markus Axel (2009)
Verification of Second-Order Functional Programs.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

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.
Konferenzveröffentlichung, Bibliographie

Aderhold, Markus ; Walther, Christoph ; Szallies, Daniel ; Schlosser, Andreas (2006)
A Fast Disprover for VeriFun.
IJCAR’06-Workshop DISPROVING’06: Non-Theorems, Non-Validity ,Non-Provability. Seattle, USA (10.08.2006-22.08.2006)
Konferenzveröffentlichung, Bibliographie

B

Bradler, Dirk ; Krumov, Lachezar ; Kangasharju, Jussi ; Mühlhäuser, Max
Hrsg.: Aguilera, M. ; Yu, H. ; Vaidya, N. ; Srinivasan, V. ; Choudhury, R. (2011)
PathFinder: Efficient Lookups and Efficient Search in Peer-to-Peer Networks.
12th International Conference on Distributed Computing and Networking (ICDCN 2011). Bangalore, India (02.01.2011-05.01.2011)
doi: 10.1007/978-3-642-17679-1_7
Konferenzveröffentlichung, Bibliographie

Bradler, Dirk ; Krumov, Lachezar ; Kangasharju, Jussi ; Weihe, Karsten ; Mühlhäuser, Max (2010)
PathFinder: Efficient Lookups and Efficient Search in Peer-to-Peer Networks.
12th International Conference on Distributed Computing and Networking. Bangalore, India (02.01.2011-05.01.2011)
doi: 10.1007/978-3-642-17679-1_7
Konferenzveröffentlichung, Bibliographie

G

Giesl, Jürgen ; Walther, Christoph ; Brauburger, J.
Hrsg.: Bibel, Wolfgang (1998)
Termination Analysis for Functional Programs.
In: Automated deduction: a basis for applications. Volume III Applications
doi: 10.1007/978-94-017-0437-3
Buchkapitel, Bibliographie

K

Katz, Shmuel ; Mezini, Mira ; Kienzle, Jörg
A Common Case Study for Aspect-Oriented Modeling.
In: Transactions on Aspect-Oriented Software Development VII, 6210
Artikel, Bibliographie

Kolbe, Thomas ; Walther, Christoph
Hrsg.: Bibel, Wolfgang (1998)
Proof Analysis, Generalization and Reuse.
In: Automated deduction: a basis for applications. Bd.2 Systems and implementation techniques
doi: 10.1007/978-94-017-0435-9
Buchkapitel, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1996)
Proving theorems by mimicking a human's skill.
The 1996 AAAI Spring Symposium. Palo Alto, USA (25.03.1996-27.03.1996)
Konferenzveröffentlichung, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1996)
Termination of theorem proving by reuse.
13th International Conference on Automated Deduction (CADE-13). New Brunswick, USA (30.07.1996-03.08.1996)
doi: 10.1007/3-540-61511-3_72
Konferenzveröffentlichung, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1995)
Patching proofs for reuse.
ECML'95: 8th European Conference on Machine Learning. Heraclion, Greece (25.04.1995-27.04.1995)
Konferenzveröffentlichung, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1995)
Second-Order Matching modulo Evaluation: A technique for Reusing Proofs.
IJCAI '95: 14th International Joint Conference on Artificial Intelligence. Montreal, Canada (20.08.1995-25.08.1995)
Konferenzveröffentlichung, Bibliographie

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.08.1995-25.08.1995)
Konferenzveröffentlichung, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1995)
Adaption of Proofs for Reuse.
1995 Fall Symposium Adaptation of Knowledge for Reuse. Cambridge, USA (10.11.1995-12.11.1995)
Konferenzveröffentlichung, Bibliographie

Kolbe, Thomas ; Walther, Christoph (1994)
Reusing Proofs.
ECAI'94: 11th European Conference on Artificial Intelligence. Amsterdam, Netherlands (08.08.1994-12.08.1994)
Konferenzveröffentlichung, Bibliographie

S

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)
doi: 10.1016/j.entcs.2006.10.038
Artikel, Bibliographie

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-21.08.2006)
Konferenzveröffentlichung, Bibliographie

Schlosser, Andreas ; Walther, Christoph ; Aderhold, Markus (2006)
Axiomatic specification in VeriFun.
IJCAR’06-Workshop Verification Workshop (VERIFY-06). Seattle, USA (15.08.2006-16.08.2006)
Konferenzveröffentlichung, Bibliographie

W

Walther, Christoph (2019)
Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base.
In: ACM Transactions on Mathematical Software (TOMS), 45 (1)
doi: 10.1145/3301317
Artikel, Bibliographie

Walther, Christoph (2018)
A Machine Assisted Proof of the Chinese Remainder Theorem.
Report, Bibliographie

Walther, Christoph (2018)
Formally Verified Montgomery Multiplication.
30th Intern. Conf. on Computer Aided Verification (CAV 2018). Oxford, UK (14.07.2018-17.07.2018)
doi: 10.1007/978-3-319-96142-2_30
Konferenzveröffentlichung, Bibliographie

Walther, Christoph ; Wasser, Nathan (2017)
Fermat, Euler, Wilson - Three Case Studies in Number Theory.
In: Journal of Automated Reasoning, 59 (2)
doi: 10.1007/s10817-016-9387-z
Artikel, Bibliographie

Walther, Christoph (2006)
A Pragmatic Approach to Equality Reasoning.
Report, Bibliographie

Walther, Christoph ; Aderhold, Markus ; Schlosser, Andreas (2006)
The L 1.0 Primer.
Report, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2005)
Automated termination analysis for incompletely defined programs.
11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004). Montevideo, Uruguay (14.03.2005-18.03.2005)
Konferenzveröffentlichung, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2005)
Reasoning about incompletely defined programs.
12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2005). Montego Bay, Jamaica (02.12.2005-06.12.2005)
doi: 10.1007/11591191_30
Konferenzveröffentlichung, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2004)
Verification in the classroom.
In: Journal of Automated Reasoning, 32 (1)
doi: 10.1023/B:JARS.0000021872.64036.41
Artikel, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2003)
About VeriFun.
19th International Conference on Automated Deduction (CADE-19). Miami Beach, USA (28.07.2003-02.08.2003)
doi: 10.1007/978-3-540-45085-6_28
Konferenzveröffentlichung, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2003)
A Machine-Verified Code Generator.
10th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-10). Almaty, Kazakhstan (22.09.2003-26.09.2003)
doi: 10.1007/978-3-540-39813-4_6
Konferenzveröffentlichung, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2002)
VeriFun user guide.
Report, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2002)
A verification of binary search.
Report, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2002)
The VeriFun tutorial.
Report, Bibliographie

Walther, Christoph ; Schweitzer, Stephan (2002)
A machine supported proof of the unique prime factorization theorem.
Report, Bibliographie

Walther, Christoph (2002)
Programmiermethodik.
In: 30 Jahre Informatik an deutschen Hochschulen: Festschrift
Buchkapitel, Bibliographie

Walther, Christoph (2001)
Semantik und Programmverifikation.
Buch, Bibliographie

Walther, Christoph ; Kolbe, Thomas (2000)
On terminating lemma speculations.
In: Information and computation, 162 (1-2)
doi: 10.1006/inco.1999.2859
Artikel, Bibliographie

Walther, Christoph ; Kolbe, Thomas (2000)
Proving theorems by reuse.
In: Artificial Intelligence, 116 (1-2)
doi: 10.1016/S0004-3702(99)00096-X
Artikel, Bibliographie

Walther, Christoph
Hrsg.: Hölldobler, S. (2000)
Criteria for termination.
In: Intellectics and computational logic: Papers in honor of Wolfgang Bibel
doi: 10.1007/978-94-015-9383-0
Buchkapitel, Bibliographie

Walther, Christoph
Hrsg.: Görz, Günther (1995)
Automatisches Beweisen.
In: Einführung in die Künstliche Intelligenz, Auflage: 2. Aufl
Buchkapitel, Bibliographie

Walther, Christoph (1994)
On Proving the Termination of Algorithms by Machine.
In: Artificial Intelligence, 71 (1)
doi: 10.1016/0004-3702(94)90063-9
Artikel, Bibliographie

Walther, Christoph
Hrsg.: Gabbay, D. M. ; Hogger, C. J. ; Robinson, J. A. (1994)
Mathematical Induction.
In: Handbook of Logic in Artificial Intelligence and Logic Programming - Volume 2: Deduction Methodologies
Buchkapitel, Bibliographie

Walther, Christoph
Hrsg.: Bajcsy, Ruzena (1993)
Combining Induction Axioms by Machine.
Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-13). Chambery, France (28.08.1993-03.09.1993)
Konferenzveröffentlichung, Bibliographie

Walther, Christoph
Hrsg.: Shapiro, Stuart S. (1992)
Mathematical Induction.
In: Encyclopedia of Artificial Intelligence-Volume 2
Buchkapitel, Bibliographie

Walther, Christoph
Hrsg.: Voronkov, Andrei (1992)
Computing Induction Axioms.
Proc. of the Inter. Conf. on Logic Programming and Automated Reasoning (LPAR-1992). St. Petersburg, Russia (15.07.1992-20.07.1992)
doi: 10.1007/BFb0013076
Konferenzveröffentlichung, Bibliographie