direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Habilitationen 2006

Habilitationsvortrag

Interaktives Theorembeweisen im Software Engineering
Dr. phil. Florian Kammüller, Technische Universität Berlin
Mittwoch, 13. Dezember 2006 um 12.00 Uhr, Raum FR 5516

In diesem Vortrag beschreiben wir verschiedene Formen wie interaktives Theorembeweisen in der Disziplin des Software-Engineering angewendet werden kann. Wir betrachten interaktives Theorembeweisen mit Higher Order Logic (HOL). HOL ist die Grundlage für die Beweiser Coq und Isabelle.

An Anwendungsbeispielen demonstrieren wir den Einsatz dieser Beweiser. Dazu stellen wir zuerst im Detail die Entwicklung einer effektiven Beschreibung von idempotenten Relationen in Isabelle/HOL vor. Danach beschreiben wir kurz den Einsatz des Beweisers Coq zur Analyse der Sicherheitseigenschaft Noninterference einer einfachen Bytecode-Sprache. Abschliessend fassen wir weitere Forschungsarbeiten zur Integration von Isabelle/HOL in den Software-Entwicklungsprozess zusammen.

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe

Diese Seite verwendet Piwik für anonymisierte Webanalysen. Mehr Informationen und Opt-Out-Möglichkeiten unter Datenschutz.