185.291 Formal Methods in Computer Science
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2022W, VU, 4.0h, 6.0EC
TUWEL

Properties

  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise
  • Format: Hybrid

Learning outcomes

After successful completion of the course, students are able to...

  • make use of basic methods of computability theory in order to identify, for instance, undecidable problems
  • apply formal methods from complexity theory to new problems in order to prove their tractability or NP-hardness,
  • represent problems in the area of formal methods as satisfiability problems, to solve these problems with a SAT solver, and to formally argue the correctness of all involved techniques and reductions,
  • formally establish partial and total correctness of software systems, by using  deductive verification approaches based on Hoare logic and predicate transformers. Students will also be able to formulate program semantics and prove program properties algorithmically,
  • understand and apply the basic techniques of model checking: encoding specifications in temporal logic, reasoning about temporal logic formulae, model checking of temporal logic formulae on Kripke structures, using state space reduction techniques, and applying bounded model checking for verification tasks.

Subject of course

Introduction to complexity theory: problem reductions, P versus NP, undecidability; SAT solving and its applications in computer science; introduction to the formal semantics of programming languages; formal verification of programs; model checking and its applications in hard- and software verification.

Teaching methods

The course is organized in four blocks. The course (and thus each block) consists of a lecture and a consolidation part.

The topics of the course are presented during the lectures.

The consolidation part includes two additional classes per block for discussing examples and their solutions. Students receive an exercise sheet for each block. The submissions will be corrected and returned to the students

Three additional classes will be offered to recall some basic principles of mathematical proofs.

Mode of examination

Written

Additional information

Ects breakdown

  2 h introduction (first meeting)
60 h lecture (20 dates à 2h + 1h preparation)
40 h exercise sheets (4 sheets, 10 exercises/sheet, 1h/exercise)
16 h discussion of exercises (8 dates à 2h)
 30 h preparation for written exam
2 h written exam
-----------------------------------------------------------
150 h = 6 Ects

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Mon13:00 - 15:0003.10.2022 - 09.01.2023EI 5 Hochenegg HS Lecture
Mon13:00 - 15:0003.10.2022 Kick-Off
Tue13:00 - 15:0011.10.2022 - 10.01.2023EI 5 Hochenegg HS Lecture
Formal Methods in Computer Science - Single appointments
DayDateTimeLocationDescription
Mon03.10.202213:00 - 15:00 Kick-Off
Mon03.10.202213:00 - 15:00EI 5 Hochenegg HS Kick-Off
Mon10.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue11.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon17.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue18.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon24.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue25.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon31.10.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon07.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue08.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon14.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon21.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue22.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon28.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue29.11.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon05.12.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue06.12.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Mon12.12.202213:00 - 15:00EI 5 Hochenegg HS Lecture
Tue13.12.202213:00 - 15:00EI 5 Hochenegg HS Lecture

Examination modalities

The evaluation is based on a written exam.

Exams

DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Tue15:00 - 18:0013.12.2022Informatikhörsaal - ARCH-INF written28.11.2022 00:00 - 09.12.2022 23:59TISSExam 3 SS
Tue15:00 - 18:0024.01.2023Informatikhörsaal - ARCH-INF written01.01.2023 00:00 - 20.01.2023 23:59TISSExan 1 WS
Fri13:00 - 16:0024.03.2023Informatikhörsaal - ARCH-INF written28.02.2023 00:00 - 20.03.2023 23:59TISSExam 2 WS
Fri13:00 - 16:0019.05.2023Informatikhörsaal - ARCH-INF written10.04.2023 09:00 - 12.05.2023 23:59TISSExam 3 WS

Course registration

Begin End Deregistration end
19.09.2022 08:00 24.10.2022 08:00 24.10.2022 08:00

Curricula

Literature

For slides and other material see the TUWEL course.

Previous knowledge

Basic knowledge in mathematical logic and algorithms are required (to the extent taught in “Theoretische Informatik und Logik” and “Algorithmen und Datenstrukturen”).

Language

English