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 (based on a GHC-implementation; replication of a proof found elsewhere)
    • Natural Mergesort (based on a GHC-implementation; direct proof)
      •   
  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 (see pdf)
    • a proof of Fermat's Little Theorem using reduced residue systems (see pdf)
    • a proof of Euler's Theorem (see pdf)
    • a proof of Wilson's Theorem (prime modulus) (see 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 (see pdf)
    • a proof of the boundedness of the smallest prime factor by the square root of a composite
      •   
  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.
    • the verification of the Boyer-Moore Fast String Search algorithm
    • the verification of the Boyer-Moore tautology checker
    • the 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
    • the verification of soundness, completeness and log-boundedness of Binary Search (see 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 (see pdf)
      •  
  8.  Folder VFR 17-01 (GHC-Mergesort) contains 5 case studies of work in progress.

_______________________________

Last update 2017-06-08