Christoph Walther:Verified Newton-Raphson Iteration for Multiplicative Inverses
Modulo Powers of Any Base. ACM Transactions on Mathematical Software (TOMS), 45(1): 9:1-9:7, 2019, https://doi.org/10.1145/3301317. See also Technical Report VFR 18/02
below. The associated proof file can be found in folder Number
Theory.
Christoph Walther: Formally Verified Montgomery Multiplication. In: H. Chockler and G. Weissenbacher (Eds.), Proc. of the
30th Intern. Conf. on Computer Aided Verification (CAV 2018), Oxford (UK), Lect. Notes in Comp. Science, vol. 10982, Springer, pp. 505-522, 2018,https://doi.org/10.1007/978-3-319-96142-2_30(open access). The associated proof file can be found in folder Number Theory.
Christoph Walther and Nathan Wasser:Fermat, Euler, Wilson - Three Case Studies in Number Theory. Journal of
Automated Reasoning, 59(2):267-286, 2017, http://dx.doi.org/10.1007/s10817-016-9387-z. View this
paper here or see Technical Report VFR 16/01 below. The proof files of the case studies presented in the
paper can be found in the folders Number Theory and VFR 16-01 Proofs.
Markus Aderhold:Second-Order Programs with Preconditions. In Simon Siegler and
Nathan Wasser, editors, Verification, Induction, Termination Analysis, vol. 6463 of Lecture Notes in Artificial Intelligence, pp. 129-143, 2010. pdf
Markus Aderhold:Automated Synthesis of Induction Axioms for Programs with Second-Order
Recur-sion. In Jürgen Giesl and Rainer Hähnle, editors, Proc. 5th International Joint Conference on Automated Rea-soning (IJCAR 2010), volume 6173 of Lecture Notes in
Artificial Intelligence, pages 263-277, Edinburgh, 2010. pdf
Markus Aderhold:Automated Termination Analysis for Programs with Second-Order Recursion. In Javier
Esparza and Rupak Majumdar, editors, Proc. 16th Intern. Conf. on Tools and Algorithms for the Construction and Analy-sis of Systems (TACAS 2010), vol. 6015 of Lecture Notes in Computer
Science, pages 221-235, Paphos, 2010. pdf
Markus Aderhold:Improvements in Formula Generalization. In Frank Pfenning, editor, Proc. 21st
Intern. Conf. on Automated Deduction (CADE-21), vol. 4603 of Lecture Notes in Comp. Science, pp. 231-246, Bremen, 2007. pdf
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
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, 2005. pdf
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 Artificial
Intelligence, pages 332—346, Montevideo, Uruguay, 2005. pdf
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, 2004. pdf
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, 2003. pdf (see folder Miscellaneous for the proof file)
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 Artificial Intelligence, pages 322—327, Miami Beach, 2003. pdf
Christoph Walther:Criteria for Termination. In S. Hölldobler, editor, Intellectics and Computational Logic, pages
361—386. Kluwer Academic Publishers, Dordrecht, 2000. ps
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
Christoph Walther:On Proving the Termination of Algorithms by Machine. Artificial Intelligence, 71(1):101—157,
1994. pdf
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, 1994. pdf
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
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 Artificial Intelligence, pages 381—392, St. Petersburg, Russia, 1992. pdf
Technical Reports
Christoph
Walther:A Machine Assisted Proof of the Chinese Remainder
Theorem. Technical Report VFR 18/03, FB Informatik, Technische Universität Darmstadt, 2018. pdf (see folder Number Theory for the proof file)
Christoph Walther:Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo
Powers of Any Base. Technical Report VFR 18/02, FB Informatik, Technische Universität Darmstadt, 2018. pdf (see folder Number Theory for
the proof file)
Christoph Walther andNathan Wasser:Fermat, Euler, Wilson - Three Case Studies in Number Theory. Technical
Report VFR 16/01, FB Informatik, Technische Universität Darmstadt, 2016. pdf (the proof files of the case studies presented in the paper can be found in the folders Number Theory and VFR 16-01 Proofs)
Christoph Walther and Stephan Schweitzer:A Pragmatic Approach to Equality Reasoning. Technical Report VFR 06/02, FB
Informatik, Technische Universität Darmstadt, 2006. pdf
Christoph Walther and Stephan Schweitzer:A Machine Supported Proof of the Unique Prime Factorization Theorem. Technical
Report VFR 02/03, FB Informatik, Technische Universität Darmstadt, 2002. pdf (see folder Number Theory for the proof file)
Christoph Walther and Stephan Schweitzer:A Verification of Binary Search. Technical Report VFR 02/02, FB Informatik,
Technische Universität Darmstadt, 2002. pdf (see folder Miscellaneous for the proof file)
System Documents
Christoph Walther, Markus Aderhold, and Andreas Schlosser: What's New in VeriFun. VeriFun Memo VFM 04/02, FB Informatik,
Technische Universität Darmstadt, 2006. pdf
Christoph Walther, Markus Aderhold, and Andreas Schlosser: The L 1.0 Primer. Technical Report VFR 06/01, FB Informatik, Technische
Universität Darmstadt, 2006. pdf
Christoph Walther and Stephan Schweitzer: The VeriFun Tutorial. Technical Report VFR 02/04, FB Informatik, Technische Universität
Darmstadt, 2002. pdf
Christoph Walther and Stephan Schweitzer: VeriFun User Guide. Technical Report VFR 02/01, FB Informatik, Technische Universität
Darmstadt, 2002. pdf (already shipped with the system)