Niels seine neue Seite
Vortrag im Seminar Spezifikation und Verifikation verteilter Systeme bei Peter Massuthe (14. Dezember 2004)
Es wird in die temporale Logik TLDA eingeführt. Anhand einer Stunden-/Minutenuhr wird das semantische Modell, die Syntax und die Semantik von TLDA erklärt. Anschließend wird gezeigt, wie verteilte Systeme mit TLDA modelliert werden können. Zu den Folien werden in einem Handout die wichtigsten Begriffe und Definitionen zusammengefasst.
Mitschrift zum 1. Teil der Vorlesung Berechenbarkeit (Wintersemester 2004/2005) bei Prof. Dr. Martin Grohe, zusammen mit Jan Bretschneider
Die Mitschrift enthält nur die Themen der ersten Semesterhälfte (bis zum 6. Dezember 2004): Berechenbare Funktionen, Nummerierung berechenbarer Funktionen, universelle Programme, entscheidbare und aufzählbare Mengen, der Kleene’sche Fixpunktsatz, die Struktur rekursiv aufzählbarer Mengen unter many-one-Reduktionen, relative Berechenbarkeit und Turingreduktionen, sowie die arithmetische Hierarchie.
Vielleicht möchte jemand diese Mitschrift irgendwann um den 2. Teil ergänzen und vervollständigen – dafür kann man hier die LATEX-Quellen herunterladen.
Vortrag im Forschungsseminar am Lehrstuhl für Theorie der Programmierung (1. Dezember 2004)
Zu der am Lehrstuhl für Theorie der Programmierung entstandene temporale Logik TLDA existiert noch kein Model Checker. Ergebnisse des Model Checkers TLC für die temporale Logik TLA haben gezeigt, wie ein Model Checker die Akzeptanz einer Modellierungssprache in der Industrie vergrößern kann. Im Vortrag werden die grundlegenden Prinzipien und Vorgehensweisen, die für die Entwicklung eines Model Checkers notwendig sind, beschrieben. Dabei stehen insbesondere Techniken aus dem Compilerbau im Mittelpunkt.
letzte Kommentare