Inhalt
[ 921SOENFMSK13 ] KV (*)Formal Methods in Software Development
|
|
|
|
| (*) Leider ist diese Information in Deutsch nicht verfügbar. |
 |
| Workload |
Ausbildungslevel |
Studienfachbereich |
VerantwortlicheR |
Semesterstunden |
Anbietende Uni |
| 4,5 ECTS |
M - Master |
Informatik |
Wolfgang Schreiner |
3 SSt |
Johannes Kepler Universität Linz |
|
|
|
| Detailinformationen |
| Quellcurriculum |
Masterstudium Computer Science 2025W |
| Lernergebnisse |
Kompetenzen |
| (*)Students can formally specify properties of sequential computer programs and
concurrent computing systems in the language of mathematical logic. They
understand the fundamental principles of the formal verification of these
properties and can apply them manually to small examples. This enables the
students to effectively utilize various software tools in order to
(semi-)automatically verify larger programs and systems.
|
|
| Fertigkeiten |
Kenntnisse |
(*)- Formal specification of program contracts (input conditions and output conditions) in first-order logic (K6).
- Derivation of verification conditions from programs that ensure that the programs satisfy their contracts (K3).
- Formulation of loop invariants and termination measures that are adequate for proving the derived verification conditions (K6).
- Formal modeling of concurrent systems as state transition systems and formal specification of system properties in linear temporal logic (K6).
- Effective use of various software tools (model checkers, extended static checkers, runtime checkers, automatic verifiers and interactive verification environments) for the verification of programs and systems that are described in abstract modeling languages or in real programming languages (K3).
|
(*)- The role of formal methods in software development.
- Formal specification and verification calculi (Hoare calculus, Dijkstra's calculus of weakest preconditions and strongest postconditions).
- Partial and total correctness.
- The role of loop invariants and termination measures in the verification process.
- Soundness and completeness of verifications.
- The Java Modeling Language (JML).
- State transition systems.
- Linear temporal logic.
- Safety and liveness properties.
- Weak and strong fairness requirements.
|
|
| Beurteilungskriterien |
(*)Running homework exercises (50%), final written exam at the end of the semester (50%).
|
| Lehrmethoden |
(*)Integrated course that combines the theoretical presentation with the practical demonstration of the application of systems on concrete examples.
|
| Abhaltungssprache |
Englisch |
| Literatur |
(*)Supporting Literature:
- Schreiner, Wolfgang: Thinking Programs, Chapter "Programs", Springer, 2021.
- Apt, Krzysztof et al: Verification of Sequential and Concurrent Programs, 3rd edition, Springer, 2009.
- 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, 2nd edition, 2004.
- Schumann, J. M.: Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001.
Special literature in the form of original papers.
|
| Lehrinhalte wechselnd? |
Nein |
| Sonstige Informationen |
(*)https://risc.jku.at/courses/
|
| Äquivalenzen |
(*)INMSPKVFMSD: KV Formal Methods in Software Development (4,5 ECTS)
|
|
|
|
| Präsenzlehrveranstaltung |
| Teilungsziffer |
- |
| Zuteilungsverfahren |
Direktzuteilung |
|
|
|
