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

2020S, VU, 4.0h, 6.0EC
TUWEL

Properties

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

Learning outcomes

Attention: The lecture will NOT take place in summer term 2020!

 

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

Die LVA is in 4 Themenblöcke unterteilt. Die LVA (und daher jeder Block) besteht aus einem Vorlesungs- und Vertiefungsteil.

Der Stoff der Lehrveranstaltung wird in den Vorlesungseinheiten präsentiert

Der Vertiefungsteil inkludiert zwei zusätzliche Lehreinheiten, die der Diskussion und dem Lösen von Übungsaufgaben dienen. Studierende erhalten für jeden Themenblock eine Übungssammlung. Ihre Lösungen werden korrigiert um Feedback zu geben.

Drei weitere Einheiten dienen einer Wiederholung grundlegender Techniken zur Beweisführung.

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

Examination modalities

The evaluation is based on a written exam.

Exams

DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Fri16:00 - 18:0016.10.2020HS 11 Paul Ludwik written05.10.2020 00:00 - 14.10.2020 08:00TISS2019 Termin 5
Wed13:00 - 15:0009.12.2020HS 11 Paul Ludwik written23.11.2020 00:00 - 07.12.2020 08:00TISS2019 Termin 6
Mon16:00 - 18:0018.01.2021GM 1 Audi. Max.- ARCH-INF written04.01.2021 00:00 - 15.01.2021 08:00TISSWS2020 Termin 1
Fri16:00 - 18:0026.03.2021HS 11 Paul Ludwik written08.03.2021 00:00 - 24.03.2021 00:00TISSWS2020 Termin 2
Fri16:00 - 18:0007.05.2021HS 11 Paul Ludwik written06.04.2021 00:00 - 03.05.2021 08:00TISSWS2020 Termin 3
Tue - 08.06.2021FH Hörsaal 1 - MWB written25.05.2021 09:00 - 03.06.2021 09:00TISSFMI Exam June 2020 - Slot 1
Tue - 08.06.2021GM 1 Audi. Max.- ARCH-INF written25.05.2021 09:00 - 03.06.2021 09:00TISSFMI Exam June 2020 - Slot 2

Course registration

Begin End Deregistration end
26.02.2020 00:00 15.03.2020 23:59 15.03.2020 23:59

Curricula

Literature

For slides end exercises see the TUWEL online course.

Miscellaneous

Language

English