623.827 (18S) Current Topics in Software Engineering: Certified Software Development
Überblick
- Lehrende/r
- LV-Titel englisch Current Topics in Software Engineering: Certified Software Development
- LV-Art Vorlesung-Kurs (prüfungsimmanente LV )
- Semesterstunde/n 2.0
- ECTS-Anrechnungspunkte 4.0
- Anmeldungen 6 (20 max.)
- Organisationseinheit
- Unterrichtssprache Englisch
- LV-Beginn 05.03.2018
- eLearning zum Moodle-Kurs
Zeit und Ort
LV-Beschreibung
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 or 622.051 Spezifikation und Verifikation.
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).
Lehrmethodik inkl. Einsatz von eLearning-Tools
The teaching method will be lectures based in classroom.
Inhalt/e
The course contents consists of lecture material (i.e. slides), tool demonstrations and associated examples based on suggested literature in "Literature" section.
Literatur
Suggested readings include
- Interactive Theorem Proving and Program Development: Coq'Art the Calculus of Inductive Constructions (1st Ed.) by Yves Bertot and Pierre Castran. Springer Publishing Company, 2010
- Certified Programming with Dependent Types (A Pragmatic Introduction to the Coq Proof Assistant) by Adam Chlipala (http://adam.chlipala.net/cpdt/)
- Software Foundations by Benjamin C. Pierce (http://www.cis.upenn.edu/~bcpierce/sf/current/index.html)
The tools required for the course include
- Coq, INRIA France (https://coq.inria.fr/)
- Why3, LRI France (http://why3.lri.fr/ - online tool available at http://why3.lri.fr/try/)
- Boogie, Microsoft USA (http://www.rise4fun.com/Boogie)
Prüfungsinformationen
Prüfungsmethode/n
The examination will be based on a group based 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).
Prüfungsinhalt/e
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.
Beurteilungskriterien/-maßstäbe
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.
Beurteilungsschema
Note BenotungsschemaPosition 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)
-
Current Topics in Software Engineering: Software Quality (
2.0h VK / 4.0 ECTS)
-
Fach: Software Engineering
(Wahlfach)