The following case studies are available for
download (see the comment in the
root folder of some of
the downloaded vffiles for additional information) :

Folder Sorting contains the verification of the sorting algorithms

Insertionsort

Bubblesort

Minimumsort

Selectionsort

Treesort

Mergesort

Quicksort

Heapsort

Natural Mergesort (also see 8. below)


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 NewtonRaphson Iteration for Multiplicative Inverses Modulo Powers of Any
Base


Folder Propositional Logic contains soundness and completeness proofs for

a sequent calculus

an implicational calculus

unit resolution for Horn clause sets

the BoyerMoore tautology checker

the DavisPutnam procedure


Folder Matching & Unification contains proofs of soundness, completeness and mostgenerality of

a firstorder matching algorithm

a firstorder unification algorithm


Folder BoyerMoore contains 3 case studies from the BoyerMoore corpus, viz.

verification of the BoyerMoore Fast String Search algorithm

verification of the BoyerMoore tautology checker

proof of the unsolvability of the Halting Problem


Folder VFR 1601 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.


Folder Miscellaneous contains

proofs of properties of the Ackermann function

verification of soundness, completeness and logboundedness 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 whileprograms (pdf)


Folder Work in progress (GHCMergesort) contains 5 case studies of work in progress.
_______________________________
Last update 20180215