This thesis presents the verification of enumeration algorithms for trees. The first algorithm is based on the well known Prüfer-correspondence and allows the enumeration of all possible labeled trees over a fixed finite set of vertices. The second algorithm enumerates rooted, unlabeled trees of a specified size up to graph isomorphism. It allows for the efficient enumeration without the use of an intermediate encoding of the trees with level sequences, unlike the algorithm by Beyer and Hedetniemi it is based on. Both algorithms are formalized and verified in Isabelle/HOL. The formalization of trees and other graph theoretic results is also presented.     «

This thesis presents the verification of enumeration algorithms for trees. The first algorithm is based on the well known Prüfer-correspondence and allows the enumeration of all possible labeled trees over a fixed finite set of vertices. The second algorithm enumerates rooted, unlabeled trees of a specified size up to graph isomorphism. It allows for the efficient enumeration without the use of an intermediate encoding of the trees with level sequences, unlike the algorithm by Beyer and Hedet...     »

Diese Arbeit beschreibt die Verifikation von Enumerationsalgorithmen von Bäumen. Der erste Algorithmus basiert auf der Prüfer-Korrespondenz und ermöglicht die Aufzählung von allen möglichen Bäumen mit einer fixen, endlichen Knotenmenge. Der zweite Algorithmus zählt gewurzelte, unbeschriftete Bäume einer gegebenen Größe bis auf Isomorphie auf. Er erlaubt eine effiziente Aufzählung ohne die Benutzung von Level-Sequenzen, anders als der Algorithmus von Beyer und Hedetniemi, welcher die Grundlage des hier beschriebenen Algorithmus ist. Beide Algorithmen werden in Isabelle/HOL formalisiert und ihre Korrektheit bewiesen. Die Formalisierung von Bäumen und andere graphentheoretische Ergebnisse werden zusätzlich vorgestellt.     «

Diese Arbeit beschreibt die Verifikation von Enumerationsalgorithmen von Bäumen. Der erste Algorithmus basiert auf der Prüfer-Korrespondenz und ermöglicht die Aufzählung von allen möglichen Bäumen mit einer fixen, endlichen Knotenmenge. Der zweite Algorithmus zählt gewurzelte, unbeschriftete Bäume einer gegebenen Größe bis auf Isomorphie auf. Er erlaubt eine effiziente Aufzählung ohne die Benutzung von Level-Sequenzen, anders als der Algorithmus von Beyer und Hedetniemi, welcher die Grundlage...     »