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


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 NewtonRaphson 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)


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

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

a verification of Dijkstra's Shortest Path Algorithm

the verification of two algorithms deciding the word problem for regular languages
_______________________________
Last update 20200612