Automatisierte Softwareverifikation erlaubt es, die Korrektheit eines Programms in Bezug auf eine gegebene Spezifikation zu beweisen und kann somit eine wertvolle Unterstützung bei der schwierigen Aufgabe der Qualitätssicherung großer Softwaresysteme sein. Jedoch stellt die zusätzliche Komplexität nichtdeterministischen Schedulings eine besondere Herausforderung für die automatisierte Verifikation nebenläufiger Software dar.

Diese Dissertation befasst sich mit Techniken zur Reduktion der Komplexität nebenläufiger Programme, um das Verifikationsproblem zu erleichtern. Wir erarbeiten dazu Lösungen aus zwei unterschiedlichen Richtungen: Zustandsraumreduktion und Reduktion von Nichtdeterminismus in Ausführungen nebenläufiger Programme.

Ersterer Richtung folgend stellen wir einen Algorithmus für Dynamic-Partial-Order-Reduction vor, einer Zustandsraumreduktion, die die Verifikation redundanter Ausführungen vermeidet. Unser Algorithmus, EPOR, erzeugt begierig (eager) Schedules für Programmfragmente. Im Vergleich zu anderen Algorithmen für Dydamic-Partial-Order-Reduction vermeidet er redundante Race- und Abhängigkeitstests. Unsere Experimente zeigen, dass EPOR deutlich schneller als ein bekannter und aktueller Algorithmus läuft, was in mehreren Fällen die Verifikation von Programmen mit mehr Threads innerhalb einer gegebenen Zeit erlaubt.

In letzterer Richtung stellen wir ein formales Framework zur Nutzung von unvollständigen Verifikationsergebnissen zur Erstellung von sicheren Schedules vor. Da unvollständige Verifikationsergebnisse nicht die Korrektheit aller möglichen Ausführungen eines Programms beweisen müssen, kann ihre Komplexität deutlich niedriger als bei vollständigen Verifikationsergebnissen sein. Dadurch können sie sehr viel schneller generiert werden. Wir schränken das Scheduling von Programmen ein, jedoch nicht ihre Eingabe, um ihre Funktionalität zu erhalten. In unserem Framework sind Ausführungen innerhalb den Schedulingbeschränkungen eines unvollständigen Verifikationsergebnisses sicher (safe), deadlockfrei und fair. Wir instantiieren unser Framework mit dem Impact Model-Checking-Algorithmus und zeigen in unserer Evaluation, dass es genutzt werden kann um Programme zu verifizieren, die nicht durch monolithisches Model-Checking handhabbar sind, um Synchronisation durch assume-Statements zu synthetisieren und um faire Ausführungen zu garantieren.

Um ein Programm sicher innerhalb der durch ein unvollständiges Verifikationsergebnisses abgedeckten Ausführungen auszuführen, muss das Scheduling beschränkt werden. Wir diskutieren, wie aus unvollständigen Verifikationsergebnissen Schedules extrahiert und encodiert werden können, sowohl für endliche als auch für unendliche Ausführungen. Zusätzlich diskutieren wir, wie Schedulingbeschränkungen effizient umgesetzt werden können, sowohl im Hinblick auf ein schnelles Nachschlagen der Erlaubnis, das nächste Event auszuführen, als auch auf die nebenläufige Ausführung unabhängiger Events (durch die Anwendung von Partial-Order-Reduction).

Ein Nachteil der Umsetzung von Schedulingbeschränkungen ist ein potenzieller Overhead in der Ausführungsdauer, jedoch erwiesen sich beschränkte Ausführungen in mehreren Fällen sogar als schneller als unbeschränkte Ausführungen. Unsere experimentellen Ergebnisse zeigen, dass das iterative Lockern von Schedulingbeschränkungen den Overhead in der Ausführungsdauer reduzieren kann. Daher ist es möglich, den erlittenen Overhead anzupassen, sodass ein optimaler Bereich im Hinblick auf die zur Erzeugung der Schedules nötigen Zeit (also die Dauer der Verifikation) gefunden wird. Interessanterweise zeigen sich Fälle, in denen durch die Wahl geeigneter Schedules der Overhead bereits viel früher reduziert werden kann, was nahelegt, dass die Ausführungsgeschwindigkeit nicht einfach nur von der Anzahl an Schedulingbeschränkungen abhängt, sondern zu einem großen Teil auch von deren Struktur.