In diesem Projekt wird eine Erweiterung klassischer Model-Checking-Techniken zur Unterstützung unendlicher Datentypen untersucht. Hierbei werden symbolische Darstellungen in Form algebraischer Beschreibungen zugrunde gelegt. Klassische Algorithmen des Model-Checkens scheitern heute meistens an der großen Menge von Daten, die in industriellem Kontext verwendet werden. Der in diesem Projekt verfolgte Ansatz reduziert die Repräsentierung von Systemzuständenunter Berücksichtigung der zu verifizierenden Eigenschaften aufalgebraische Darstellungen von Systemeigenschaftenund integriert diese in sogenanntes symbolisches Model-Checken, eine der prominentesten klassischen Methoden.Als wesentliches Ziel konnte die praktische Umsetzung und Erprobung der algebraischen Erweiterung des symbolischen Model-Checkens erreicht werden. Für die Erprobung boten sich industrielle Fallstudien an, die aus verschiedenen Projekten vorliegen. Sie stammen aus den Bereichen Avionik und Automobilelektronik. Aufgrund der ersten Erfahrungen wurde der entwickelte Prototyp optimiert. Optimierungskriterium ist dabei zum einen eine höhere Effizienz, d. h. eine Verkürzung der Verifikationslaufzeiten. Zum anderen stand und steht aber die Anwendbarkeit auf große industrielle Fallstudien im Vordergrund. Das heißt auch, dass die Integration algebraischer Techniken nicht losgelöst von der Anwendungsumgebung gesehen werden kann. Die Integration der algebraischen Darstellung von Systemeigenschaften ist nicht mehr allein eine Aufgabe des symbolischen Modelcheckers, sondern eine Integration in die gesamte Verifikations-Tool-Kette und Verifikationsmethodik. Hier hat sich die Zielsetzung aufgrund der gemachten Erfahrungen von einem Spezialverfahren hin zu einem durchgängigen Konzept verändert.