Correct-by-Construction Software Engineering - Einzelansicht

The course (shortname CbC-SE_25_26) is organised in Moodle.

Participants should have at least basic knowledge of Logics and the C programming language.

Helpful, but not necessary, is experience with functional programming languages (as OCaml).

As side requirement (PNL), participants have to pass the exercises, i.e. achieve at least 50 % of the exercise points, according to the module decription. The exam is planned to be an oral examination.

• Bugs in Software
• Correctness of Software
• Functional Properties of Software (Specification)
• Working with the proof assistant Rocq (Coq)
• Data types in Rocq
• Defining programs in Rocq (functional model)
• Proving properties of programs
• Synthesising correct-by-construction programs from specifications
• Performance of synthesised programs
• Extracting programs into functional (OCaml) and imperative languages (C)
• Interfacing extracted C-Code and OCaml-Code with handwritten code

Students interested in formalising, verifying and synthesising software with correctness guarantees.