623.827 (17S) Current Topics in Software Engineering: Certified Software Development
- LV-Titel englisch
- Current Topics in Software Engineering: Certified Software Development
- Vorlesung-Kurs (prüfungsimmanente LV )
- 6 (20 max.)
- zum Moodle-Kurs
Zeit und Ort
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.
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
- 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
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.
Position im Curriculum
- Masterstudium Angewandte Informatik
(SKZ: 911, Version: 13W.1)
Fach: Software Engineering
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)