Inhalt

[ 921SOENFMSK13 ] KV (*)Formal Methods in Software Development

Versionsauswahl
(*) Leider ist diese Information in Deutsch nicht verfügbar.
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
Quellcurriculum Masterstudium Computer Science 2022W
Ziele (*)Students understand the basic concepts of the formal specification of programs and systems and of the formal reasoning about the correctness of implementations with respect to the specification. They are able to formally specify programs and systems and to apply concrete software tools in order to ensure the correctness with respect to the specification.
Lehrinhalte (*)Role of formal methods in software development, specification and verification of imperative programs (Hoare calculus, Dijkstra's calculus of weakest preconditions and strongest postconditions, relational calculus), specification and verification of Java programs (Java Modeling Language JML), specification and verification of concurrent systems (transition systems, temporal logic); practical application of model checkers (RISCAL), runtime checkers (JML/OpenJML), extended static checkers (ESC/Java2), automatic verification systems (OpenJML), integrated verification environments (RISC ProgramExplorer, KeY), model checkers for concurrent systems (Spin).
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