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) :
-
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 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)
-
-
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
-
-
Folder Matching & Unification contains proofs of soundness, completeness and most-generality of
-
a first-order matching algorithm
-
a first-order unification algorithm
-
-
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
-
-
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.
-
-
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