Menü
Positionsanzeige
Inhalt

[ 921SOENFMSK13 ] KV Formal Methods in Software Development
Versionsauswahl
Workload Education level Study areas Responsible person Hours per week Coordinating university
4,5 ECTS M - Master's programme Computer Science Wolfgang Schreiner 3 hpw Johannes Kepler University Linz
Detailed information
Original study plan Master's programme Computer Science 2025W
Learning Outcomes
Competences
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.
Skills Knowledge
  • 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.
Criteria for evaluation Running homework exercises (50%), final written exam at the end of the semester (50%).
Methods Integrated course that combines the theoretical presentation with the practical demonstration of the application of systems on concrete examples.
Language English
Study material 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.

Changing subject? No
Further information https://risc.jku.at/courses/
Corresponding lecture INMSPKVFMSD: KV Formal Methods in Software Development (4,5 ECTS)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment