Inhalt
[ INMSPKVFMSD ] KV (*)Formal Methods in Software Development
|
|
|
|
| (*) Unfortunately this information is not available in english. |
 |
| Workload |
Education level |
Study areas |
Responsible person |
Hours per week |
Coordinating university |
| 4,5 ECTS |
M1 - Master's programme 1. year |
Computer Science |
Wolfgang Schreiner |
3 hpw |
Johannes Kepler University Linz |
|
|
|
| Detailed information |
| Pre-requisites |
(*)Empfohlen: Grundkenntnisse der Prädikatenlogik und Grundkenntnisse der Programmierung
|
| Original study plan |
Master's programme Software Engineering (discontinuing) 2012W |
| Objectives |
(*)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.
|
| Subject |
(*)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)
|
| Criteria for evaluation |
(*)Übungsaufgaben (50%), Abschlussklausur (50%)
|
| Language |
German |
| Study material |
(*)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
|
| Changing subject? |
No |
|
|
|
| On-site course |
| Maximum number of participants |
35 |
| Assignment procedure |
Direct assignment |
|
|
|
