Homepage
Sitemap
Kontakt




Universität Bremen Universität Bremen Fachbereich 3 Informatik
Home « Lehre « Lehrmaterial


Methoden der Verifikation (03-701.06) 

Veranstalter: Prof. Dr. Rolf Drechsler

Dieses Seminar geht der Frage nach, wie die Korrektheit von Schaltungen nachgewiesen werden kann. Im Gegensatz zur Simulation von Schaltungen, deren Grenze z.B. durch den Pentium-Bug aufgezeigt wurde, ist das Ziel der formalen Verfikation der Korrektheitsbeweis.

Formale Verifikation lässt sich in zwei Bereiche einordnen:
Äquivalenzvergleich und Modellprüfung.

Es sollen aus beiden Gebieten Verfahren vorgestellt werden. Wichtige Techniken hierbei sind die effiziente Repräsentation von Booleschen Funktionen (DDs) und SAT-Solver. Im Rahmen der Verfahren zur Modellprüfung sollen temporale Logiken, wie z.B. CTL und LTL, betrachtet werden.

Ausgehend von einer kurzen Einführung über den Hardware-Entwurfprozess soll das Seminar bis zur aktuellen Forschung führen.

Termin und Ort nach Vereinbarung mit Prof. Dr. Rolf Drechsler.



Hinweise zum Seminar (pdf)
Schein (pdf)
Thema
Vortragende
Ausarbeitung
Folien
Der SAT-Beweiser CIRCUS S. Meyer pdf pdf
Das Verifikationssystem GUIDO Deng Zhou pdf pdf
Lösung von Integer Linear Programs A. Kaib, O. Heid pdf pdf
Alles als Archiv tgz



 Entnehmen Sie Angaben bezügl. Ort und Zeit bitte der Lehrveranstaltungs-Liste der Universität Bremen



[Folien (außer Übungsblätter) nur aus dem Campusnetz erreichbar]






zurück





English









Zum Seitenanfang Zur Homepage
Zur Sitemap
Kontakt