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

Sommersemester 2017

Registration deadline has expired.

First course session
06.03.2017 08:30 - 10:00 S.1.42 On Campus
... no further dates known

Overview

Lecturer
Course title german Current Topics in Software Engineering: Certified Software Development
Type Lecture - Course (continuous assessment course )
Hours per Week 2.0
ECTS credits 4.0
Registrations 6 (20 max.)
Organisational unit
Language of instruction English
Course begins on 06.03.2017
eLearning Go to Moodle course

Time and place

List of events is loading...

Course Information

Intended learning outcomes

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).

Teaching methodology including the use of eLearning tools

The teaching method will be based in classroom.

Course content

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

Literature

Suggested readings include

The tools required for the course include

Examination information

Im Fall von online durchgeführten Prüfungen sind die Standards zu beachten, die die technischen Geräte der Studierenden erfüllen müssen, um an diesen Prüfungen teilnehmen zu können.

Examination methodology

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).

Examination topic(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.

Assessment criteria / Standards of assessment for examinations

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.

Grading scheme

Grade / Grade grading scheme

Position in the curriculum

  • Master's degree programme Applied Informatics (SKZ: 911, Version: 13W.1)
    • Subject: Software Engineering (Compulsory elective)
      • 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)

Equivalent courses for counting the examination attempts

This course is not assigned to a sequence of equivalent courses