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 (based on a GHCimplementation; replication of a proof found elsewhere)

Natural Mergesort (based on a GHCimplementation; direct proof)


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

a proof of Bézout's Lemma

a proof verifying the correctness of Montgomery Multiplication


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.

the verification of the BoyerMoore Fast String Search algorithm

the verification of the BoyerMoore tautology checker

the 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

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


Folder
VFR 1701 (GHCMergesort) contains 5 case studies of work in progress.
_______________________________
Last update 20170730