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.

2022S, VU, 4.0h, 6.0EC
TUWEL

Properties

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

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 4 blocks; each block consists of a lecture and consolidation part.

Lectures are provided via pre-recorded videos.

The consolidation part of each block has 3 live-lectures, in order to dicuss and solve examples. Students receive for each block a set of examples they have to solve. They receive individual feedback to their solutions.

Three additional classes are provided to recall basic proof techniques.


 

 

Please note: Depending on the currently required Covid measures, Q+A sessions might be online via Tuwel instead of in the lecture hall. Exams might be postponed or done via TUWEL.

 

 

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
Wed10:00 - 11:0002.03.2022 via Zoom (LIVE)Kick-Off Meeting
Wed09:00 - 11:0009.03.2022 - 22.06.2022FAV Hörsaal 1 - INF Q+A Sessions
Fri13:00 - 15:0011.03.2022 - 17.06.2022FAV Hörsaal 1 - INF Q+A Sessions
Formal Methods in Computer Science - Single appointments
DayDateTimeLocationDescription
Wed02.03.202210:00 - 11:00 via ZoomKick-Off Meeting
Wed09.03.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri11.03.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed16.03.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri18.03.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed23.03.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri25.03.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed30.03.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri01.04.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed06.04.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri08.04.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed27.04.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri29.04.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed04.05.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri06.05.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed11.05.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri13.05.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed18.05.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions
Fri20.05.202213:00 - 15:00FAV Hörsaal 1 - INF Q+A Sessions
Wed25.05.202209:00 - 11:00FAV Hörsaal 1 - INF Q+A Sessions

Examination modalities

The evaluation is based on a written exam.

Exams

DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Fri13:00 - 16:0028.10.2022Informatikhörsaal - ARCH-INF written07.10.2022 00:00 - 25.10.2022 23:59TISSExam 2 SS
Fri13:00 - 16:0023.12.2022Informatikhörsaal - ARCH-INF written06.12.2022 00:00 - 20.12.2022 23:59TISSExam 3 SS
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
17.02.2022 00:00 20.03.2022 23:59 20.03.2022 23:59

Curricula

Literature

For slides end exercises see the TUWEL online course.

Miscellaneous

Language

English