Mathematical Logic and Formal Methods

Module Code
Module Coordinators
Berthold Franzen
  • Berthold Franzen
  • Burkhardt Renz
  • Short Description
    The module treats basic concepts, notions, methods and tools for the practical application of formal methods for correct modelling of sequential and concurrent systems.
    Learning Objectives

    The students know basic concepts and notions, which enable them to practically apply formal methods for correct modelling of sequential and concurrent systems. They are able to choose from numerous analysis techniques and modelling approaches those which are suited best to investigate relevant system properties by means of a model.

    • Propositional logic: language, semantics, natural deduction, normal forms, decision questions, SAT solver, applications in software engineering with MPA (MNI Proposition Analyzer)
    • first order logic: language, semantics, natural deduction, decision problems, expressive power of fol, micro models of software with Alloy
    • Temporal logic: language of linear temporal logic (LTL), semantics, decision questions, model checking with Spin
    Duration in Semester
    Instruction Language
    Total Effort
    6 CrP; an estimated 180 hours, of which approximately 60 are spent in class.
    Weekly School Hours
    Method of Instruction
    Lecture 2 sppw Exercises 2 sppw
    Requirements for the awarding of Credit Points
    Written exam
    Evaluation Standard
    according to examination regulations (§ 9)
    • M. Huth, M. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems Cambridge University Press
    • M. Ben-Ari: Mathematical Logic for Computer Science Springer
    • M. Schenker: Logikkalküle in der Informatik Springer Vieweg
    • B. Renz: Lösungen mit dem MNI Proposition Analyzer MPA Technischer Bericht Fachhochschule Gießen-Friedberg
    • D. Jackson: Software Abstractions: Logic, Language, and Analysis MIT Press
    • M. Ben-Ari: Principles of the Spin Model Checker Springer
    Prerequisite for Modules