Case Studies

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

root folder of some of the downloaded vf-files for additional information) :

        1. Folder Sorting contains the verification of the sorting algorithms

          • Insertionsort
          • Bubblesort
          • Minimumsort
          • Selectionsort
          • Treesort
          • Mergesort
          • Quicksort
          • Heapsort
          • Natural Mergesort (also see 8. below)
        2. Folder Number Theory contains

          • proofs of inequations and series (Textbook Exercises)
          • a proof of the irrationality of the square root of 2
          • 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
          • 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
          • a verification of Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base
        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
          • verification of soundness, completeness and log-boundedness of Binary Search (pdf)
          • verification of a recursive decent analyzer for a small LL(1)-grammar
          • verification of a code generator generating machine code from while-programs (pdf)
        8.  Folder Work in progress (GHC-Mergesort) contains 5 case studies of work in progress.



Last update 2018-04-06