Inhalt

[ INMSPKVFMSD ] KV Formal Methods in Software Development

Versionsauswahl
Workload Ausbildungslevel Studienfachbereich VerantwortlicheR Semesterstunden Anbietende Uni
4,5 ECTS M1 - Master 1. Jahr Informatik Wolfgang Schreiner 3 SSt Johannes Kepler Universität Linz
Detailinformationen
Anmeldevoraussetzungen Empfohlen: Grundkenntnisse der Prädikatenlogik und Grundkenntnisse der Programmierung
Quellcurriculum Masterstudium Software Engineering (auslaufend) 2012W
Ziele Die Studierenden verstehen die grundlegenden Konzepte der formalen Spezifikation von Programmen und Systemen sowie des formalen Schließens über die Korrektheit von Implementierungen in Bezug auf die Spezifikation. Sie sind befähigt, Software-Werkzeuge, die diesen Prozess unterstützen, anzuwenden.
Lehrinhalte Rolle formaler Methoden in der Software-Entwicklung; Spezifikation und Verifikation imperativer Programme; Spezifikation und Verifikation von Java Programmen; Spezifikation und Verifikation von nebenläufigen Systemen, Beweis-Assistenten (z.B. RISC ProofNavigator), statische Checker (z.B. ESC/Java2, KeY), Model Checker (z.B. SPIN)
Beurteilungskriterien Übungsaufgaben (50%), Abschlussklausur (50%)
Abhaltungssprache Deutsch
Literatur Basisliteratur:
 Schumann, J. M.: Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001.
 Beckert, B.; Hähnle, R.; Schmitt, P. H. (Eds.): Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, 2007.
 Huth, M.; Ryan, M.: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, in der aktuellen Auflage.

Ergänzungsliteratur wird in jedem Semester bekannt gegeben

Lehrinhalte wechselnd? Nein
Präsenzlehrveranstaltung
Teilungsziffer 35
Zuteilungsverfahren Direktzuteilung