Große Systeme können in der Praxis nur durch die Kombination
verschiedener Verifikations- und Spezifikationsmethoden verifiziert werden.
Algorithmische Methoden können endliche Systeme nur bis zu
einer bestimmten Größe überprüfen, während deduktive Methoden nur für
Spezifikationen geringer Komplexität geeignet sind, weil sie von intensiver
Benutzerinteraktion abhängig sind.
Die einzige Hoffnung, formale
Verifikation für Probleme von industrieller Größe einzusetzen, baut
auf die Anwendung zweier wichtiger Prinzipien: Kompositionalität und
Abstraktion.
In der Vorlesung ``Verifikation nebenläufiger Programme'' wurde
Kompositionalität behandelt. In diesem Seminar wird das Prinzip der
Abstraktion behandelt.
Die Vorlesung ``Verifikation nebenläufiger Programme'' ist keine
Vorraussetzung für das Seminar.
Das Seminar richtet sich an Studierende im Hauptstudium. In dem Seminar
werden Forschungsartikel bzgl. Abstraktion behandelt. Diese werden in der
Vorbesprechung verteilt.
Mögliche Vortragsthemenbereiche sind
Abstraktion allgemein
Abstraktion von labeled tranition system
abstrakte Interpretation
Vorträge
Termin
Vortragender
Thema
Quelle
Folien
Table 1: Vorträge (bislang vergebene Themen)
Anmeldung
Am besten per email oder vorbeikommen.
Scheinkriterium
Verlangt ist die Ausarbeitung eines Vortrags (mit Hilfestellung natürlich) und
seine Präsentation über das gewählte Thema. Relevant sind
Beherrschung des Themas sowie
Klarheit, Angemessenheit etc. der Präsentation.
Daneben wird regelmäßige Teilnahme am Seminar vorrausgesetzt.
![[Christian-Albrechts-Universität]](../../images/cau_logo.gif){kind=logo}
![[Technical Faculty]](../../images/tflogo.gif){kind=small}