Christoph Walther

ACM Trans. Math. Softw., 2019

2018

Formally Verified Montgomery Multiplication.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Fermat, Euler, Wilson - Three Case Studies in Number Theory.

[BibT_eX]

[DOI]

Nathan Wasser

J. Autom. Reason., 2017

2006

Context Dependent Procedures and Computed Types in -eriFun.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages meets Program Verification, 2006

2005

Reasoning About Incompletely Defined Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

2004

Verification in the Classroom.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

Automated Termination Analysis for Incompletely Defined Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2003

A Machine-Verified Code Generator.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

About VeriFun.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

Automatisches Beweisen.

[BibT_eX]

[DOI]

Proceedings of the Handbuch der Künstlichen Intelligenz, 4. Auflage, 2003

2001

Semantik und Programmverifikation

[BibT_eX]

Teubner Texte zur Informatik 34, Teubner, ISBN: 3-519-00336-8, 2001

2000

On Terminating Lemma Speculations.

[BibT_eX]

[DOI]

Inf. Comput., 2000

Proving theorems by reuse.

[BibT_eX]

[DOI]

Artif. Intell., 2000

Criteria for Termination.

[BibT_eX]

Proceedings of the Intellectics and Computational Logic (to Wolfgang Bibel on the occasion of his 60th birthday), 2000

1996

Termination of Theorem Proving by Reuse.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs.

[BibT_eX]

[DOI]

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

Patching Proofs for Reuse (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Machine Learning: ECML-95, 1995

1994

On Proving the Termination of Algorithms by Machine.

[BibT_eX]

[DOI]

Artif. Intell., 1994

Reusing Proofs.

[BibT_eX]

Proceedings of the Eleventh European Conference on Artificial Intelligence, 1994

Mathematical induction.

[BibT_eX]

Proceedings of the Handbook of Logic in Artificial Intelligence and Logic Programming, 1994

1993

Combining Induction Axioms by Machine.

[BibT_eX]

[DOI]

Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

1992

Computing Induction Axioms.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning, 1992

1991

Automatisierung von Terminierungsbeweisen.

[BibT_eX]

Vieweg, ISBN: 3-528-04771-2, 1991

1989

Many-Sorted Inferences in Automated Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Sorts and Types in Artificial Intelligence, 1989

1988

Many-sorted unification.

[BibT_eX]

[DOI]

J. ACM, 1988

Argument-Bounded Algorithms as a Basis for Automated Termination Proofs.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Many-Sorted Resolution.

[BibT_eX]

[DOI]

Proceedings of the Künstliche Intelligenz, 5. Frühjahrsschule, 1987

A Many-Sorted Calculus Based on Resolution and Paramodulation.

[BibT_eX]

Pitman / Morgan Kaufmann, ISBN: 0-273-08718-5, 1987

1986

Automatisches Beweisen.

[BibT_eX]

[DOI]

Proceedings of the Künstliche Intelligenz, 1986

A Classification of Many-Sorted Unification Problems.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

The Karlsruhe Induction Theorem Proving System.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution.

[BibT_eX]

[DOI]

Artif. Intell., 1985

1984

Unification in Many-Sorted Theories.

[BibT_eX]

Proceedings of the Advances in Artificial Intelligence, 1984

1983

A Many-Sorted Calculus Based on Resolution and Paramodulation.

[BibT_eX]

[DOI]

Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

1982

A many-sorted calculus based on resolution and paramodulation.

[BibT_eX]

[DOI]

PhD thesis, 1982

1981

Elimination of Redundant Links in Extended Connection Graphs.

[BibT_eX]

[DOI]