623.827 (17S) Current Topics in Software Engineering: Certified Software Development

Sommersemester 2017

Anmeldefrist abgelaufen.

Erster Termin der LV
06.03.2017 08:30 - 10:00 , S.1.42
... keine weiteren Termine bekannt


LV-Titel englisch
Current Topics in Software Engineering: Certified Software Development
Vorlesung-Kurs (prüfungsimmanente LV )
6 (20 max.)
zum Moodle-Kurs


Intendierte Lernergebnisse

What this course is about

In general, this course will introduce an approach that allows software engineer to build "certified" software like other traditional engineering disciplines, by providing a mathematical foundation for rigorous analysis of computer programs. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave correctly. As other engineering disciplines have their computer-aided-design tools, software engineering has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected.

In particular, we will learn the Why3 verification framework and Coq proof assistant to develop "certified" computer systems by employing logical reasoning using (automatic and interactive) theorem proving.

Importantly, the course will introduce practical tools for the verification of industrial applications on one hand and will introduce new scientific and research questions about practical verification techniques, on the other hand. 

This course is also suitable for those who took (or want to take) 622.050 Spezifikation und Verifikation. I will teach 622.050 in WS17 with totally different but state-of-the-art topics/tools in the subject area.

Learning outcome

The learning outcome of the course includes

  • Mastering the application of formal methods to design and develop "certified" programs,
  • Learning existing  (programming) tools based on formal methods to develop such systems, specifically Why3 (optionally Boogie),
  • Understanding background methods and techniques, specifically automatic theorem proving and
  • Learning advanced tools, specifically Coq (including interactive theorem proving).


The teaching method will be based in classroom.


The course contents consists of lecture material (i.e. slides), tool demonstrations and associated examples based on suggested literature in "Literature" section.


Suggested readings include

The tools required for the course include



The examination will be based on a group based or individual project. Optionally, the project can be developed by an individual.

Importantly, the project will include many sub-tasks, each corresponding to different lecture unit(s).


The examination project will include

  • developing project task in a language of your choice (e.g. Java, C#) AND using the tools (i.e. Why3) that we will learn during the course and
  • sharing your experience of developing these two projects in the last lecture.

Remember, the project topics will be provided and respectively assigned in the first couple of lectures.


In principle,  we will evaluate the theoretical and practical learning of the concepts introduced in the course. Specifically, the assessment criteria includes

  • development of the assigned project goal(s),
  • analysis of the development and
  • presentation of the project.


Note/Grade Benotungsschema

Position im Curriculum

  • Masterstudium Angewandte Informatik (SKZ: 911, Version: 13W.1)
    • Fach: Software Engineering (Wahlfach)
      • Current Topics in Software Engineering: Software Quality ( 2.0h VK / 4.0 ECTS)
        • 623.827 Current Topics in Software Engineering: Certified Software Development (2.0h VC / 4.0 ECTS)

Gleichwertige Lehrveranstaltungen im Sinne der Prüfungsantrittszählung

Diese Lehrveranstaltung ist keiner Kette zugeordnet