Module Import 04IN2002 - Formal Specification and Verification

Status: Published
Workload6 ECTS = 180 hrs
Credits, Weight6 ECTS, (n.s.)
Language of Instruction German or English
Semester (n.s.)
Duration1 Sem.
M/E Elective
Courses
Course No. Type Name MA/EL Workload Credits Contact Hours Selfstudy Group Size
04IN2002-1 Lecture Formal Specification and Verification EL 4.5 ECTS = 135 hrs - 3 hrs/week = 45 hrs 90 hrs 30
04IN2002-2 Exercise Formal Specification and Verification EL 1.5 ECTS = 45 hrs - 1 hrs/week = 15 hrs 30 hrs 30
Learning Outcomes

The students know various methods and languages for the formal specification of software and can apply them practically.
They know various software verification techniques and understand their logical fundaments.
They can formal verify program correctness applying corresponding tools.

Content

(not specified)

04IN2002-1 - Formal Specification and Verification

1. Introduction

  • Propositional logic, Predicate logic: Recapitulation

2. Specification and Analysis

  • Model-based specification
  • Algebraic specification
  • Declarative modelling

3. Verification

  • Logics for program verification:
    • Hoare Logic, Dynamic Logic, Temporal Logic
  • Model Checking
  • Deductive Verification, Software Model Checking

4. Applications, Examples

04IN2002-2 - Formal Specification and Verification

In the exercises for the lecture "Formal Specification and Verification" the material presented in the lectures is repeated in order to achieve a thorough understanding. Solutions to exercises related to the topics of the lectures are presented and discussed by the students.

Teaching Methods

Lecture with interactive elements.

Exercise: The students present the results of their work; Discussions; Solving exercises

Prerequisites

Basic knowledge of Logic: Propositional Logic, Predicate logic as taught in the lecture "Logic for computer scientists".

The book of Uwe Schöning "Logik für Informatiker", 5. Auflage. Spektrum Akademischer Verlag, 2000 covers the prerequisites sufficiently.

Examination Methods

Oral or written exam, depending on the number of participants

Weight of the grade in the final grade for Lehramt Gymnasium: 5% corresponding to LP (6:120); for Lehramt Realschule: 10% corresponding to LP (6:60)

Credit Requirements

(not specified)

References

(not specified)

04IN2002-1 - Formal Specification and Verification

Peter H. Schmitt. Formal Specification and Verification. Skriptum zur Vorlesung. Universität Karlsruhe, 2005.

Michael Huth, Mark Dermot Ryan: Logic in computer science - modelling and reasoning about systems Cambridge University Press 2004.

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking, The MIT Press 2008.

Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.

Jose Bacelar Almeida, Maria Joao Frade, Jorge Sousa Pinto and Simao Melo de Sousa. Rigorous Software Development: An Introduction to Program Verification, Springer Verlag, 2011.

Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

Use of this Module
  1. unmodified as Elective  -    BSc Computer Science 2017  -    Mandatory elective courses Computer Science  -    Formal Specification and Verification
  2. unmodified as Elective  -    BSc Computational Visualistics 2017  -    Mandatory elective courses Computer Science  -    Formal Specification and Verification
  3. unmodified as Elective  -    BSc Computational Visualistics 2017  -    Mandatory elective courses in Computational Visualistics or computer science  -    Formal Specification and Verification
  4. unmodified as Elective  -    MSc Computer Science 2017  -    Mandatory elective courses in mathematics and theoretical computer science  -    Formal Specification and Verification
  5. unmodified as Elective  -    MSc Computer Science 2017  -    Mandatory elective courses Computer Science  -    Formal Specification and Verification
  6. unmodified as Elective  -    MSc Computer Science 2017  -    Major subject computer science  -    Data and Knowledge Engineering  -    Formal Specification and Verification
  7. unmodified as Elective  -    MSc Computer Science 2017  -    Major subject computer science  -    Software Engineering  -    Formal Specification and Verification
  8. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses Computer Science  -    Formal Specification and Verification
  9. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in Computational Visualistics or computer science  -    Formal Specification and Verification
  10. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in theoretical computer science and mathematics  -    Formal Specification and Verification
  11. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in theoretical computer science and mathematics or natural and social sciences  -    Formal Specification and Verification
  12. unmodified as Elective  -    MSc Information Systems 2017  -    Mandatory elective courses Application Systems in Business and Administration  -    Formal Specification and Verification
Responsible / Organizational Unit
Sofronie-Stokkermans, Viorica / Institute for Computer Science
Additional Information

(not specified)

Last change
Apr 24, 2018 by Frey, Johannes
Last Change Module
Sep 19, 2018 by Frey, Johannes