Inhalt
[ INMSPKVFMSD ] KV Formal Methods in Software Development
|
|
|
|
 |
| 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 |
|
|
|
