1. Documents

Papers and Reports

 

Publications

  • 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 and Nathan 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)

_______________________________

Last update 2019-02-27