1. Case Studies

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
      •   

  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