Verification of Combinatorial Algorithms

Chair for Logic and Verification

Bachelor’s/Master’s thesis

The aim is to verify a library of algorithms for listing combinatorial objects: permutations, subsets, partitions, trees, … . There is a rich literature on the subject (see below). Part of the challenge is to find elegant functional programs instead of the universally imperative algorithms given in the literature (Nijenhuis and Wilf even give Fortran programs!). You can find a first Isabelle example here

[1] Knuth, The Art of Computer Programming, Volume 4A, Combinatorial Algorithms

[2] Nijenhuis and Wilf. Combinatorial Algorithms

[3] Stanton and White. Constructive Combinatorics

Prerequisites: Some familiarity with Isabelle/HOL.

Supervisor: Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []