### Case Studies

The following case studies are available for download (see the comment in the

1. Folder Sorting contains the verification of the sorting algorithms

• Insertionsort
• Bubblesort
• Minimumsort
• Selectionsort
• Treesort
• Mergesort
• Quicksort
• Heapsort
• Natural Mergesort
•
2. Folder Number Theory contains

• proofs of inequations and series (Textbook Exercises)
• a proof of the irrationality of the square root of any prime number
• a proof of the Binomial Theorem and some properties of Binomial Coefficients
• a verification of Eratosthenes' method for computing all primes in a given interval
• a proof of Fermat's Little Theorem using the Binomial Theorem (pdf)
• a proof of Fermat's Little Theorem using reduced residue systems (pdf)
• a proof of Euler's Theorem (pdf)
• a proof of Wilson's Theorem (prime modulus) (pdf)
• a proof of Wilson's Theorem (composite modulus)
• a verification of the RSA encryption method
• a proof of the infinitude of primes using Euclid's method
• a proof of the infinitude of primes using Fermat Numbers
• two proofs of the infinitude of primes using the factorial function
• a proof of the infinitude of primes using pronic numbers
• a proof of soundness, completeness and uniqueness of prime factorization (pdf)
• a proof of the boundedness of the smallest prime factor by the square root of a composite
• a proof of Bézout's Lemma (extended Euclidean algorithm)
• a verification of Montgomery Multiplication (pdf)
• a verification of Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base (pdf)
• the verification of a test for (non-)divisibility of numbers by considering the residues of their cross sums in a positional numeral system
• a proof of the Chinese Remainder Theorem (pdf)
•
3. Folder Propositional Logic contains soundness and completeness proofs for

• a sequent calculus

• an implicational calculus

• unit resolution for Horn clause sets

• the Boyer-Moore tautology checker

• the Davis-Putnam procedure

•
4. Folder Matching & Unification contains proofs of soundness, completeness and most-generality of
• a first-order matching algorithm
• a first-order unification algorithm
•
5. Folder Boyer-Moore contains 3 case studies from the Boyer-Moore corpus, viz.
• verification of the Boyer-Moore Fast String Search algorithm
• verification of the Boyer-Moore tautology checker
• proof of the unsolvability of the Halting Problem
•
6. Folder VFR 16-01 Proofs contains 3 case studies from the paper Fermat, Euler, Wilson - Three Case Studies in Number Theory.
• The remaining case studies of the paper are collected in the folder Number Theory above.
•
7. Folder Miscellaneous contains
• proofs of properties of the Ackermann function
• a verification of soundness, completeness and log-boundedness of Binary Search (pdf)
• the verification of a recursive decent analyzer for a small LL(1)-grammar
• the verification of a code generator generating machine code from while-programs (pdf)
• a verification of Dijkstra's Shortest Path Algorithm
• the verification of two algorithms deciding the word problem for regular languages

_______________________________

Last update 2020-06-12