185.A93 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, UE, 2.0h, 3.0EC
TUWELLectureTubeQuinn ECTS survey


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: UE Exercise
  • LectureTube course
  • Format: Presence

Learning outcomes

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

  • ... formalise Problems as SAT or SMT problems,
  • ... to solve the formalistaions with Z3,
  • ... solve combinbatorial problems via a reduction und SAT-solving tools,
  • ... to apply deductive verification methods based on Hoare logic and predica transformers, 
  • ... to establish partial/total correctness of software using deductive verification methods and tools,
  • ... to apply model checking: to create a model of the system that needs to be verified, to formalize the specification as a formula in temporal logic, and to interpret possible counterexamples.

Subject of course

This course deepens the understanding of the topics in the course "6.0 VU Formal Methods in Computer Science" by offering additional exercises. The course presents exercises for the following topics:

  • Complexity theory: NP-completeness, undecidability, reduction of problems
  • Satisfiability problems: SAT, SMT
  • Partial/total correctness of programs: Hoare calculus, weakest precondition, strongest postcondition
  • Formal verification based on model checking

Teaching methods

For each of the topics, there is an exercise sheet.

  • Each of the exercises sheets will be presented in a dedicated class.
  • Students are supposed to work on these exercises autonomously and submit their solutions in tuwel.
  • There will be a class where student solutions and an example solution are discussed.

Mode of examination


Additional information


Kick-off: 3.10.2022, 13:00 (together via VU, EI5)



Course dates

Wed13:00 - 15:0019.10.2022 - 18.01.2023FAV Hörsaal 1 - INF FMI UE
Formal Methods in Computer Science - Single appointments
Wed19.10.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed09.11.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed16.11.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed30.11.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed07.12.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed14.12.202213:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed11.01.202313:00 - 15:00FAV Hörsaal 1 - INF FMI UE
Wed18.01.202313:00 - 15:00FAV Hörsaal 1 - INF FMI UE

Examination modalities

The submitted solutions to each of the exercise sheets are graded, on a scale of 0-15 points each. The scoring depends on the correctness of the solutions as well as the on the quality of writing of the accompanying report. The final grad is by the sum of the points for the individual exercise sheets.

Course registration

Begin End Deregistration end
02.10.2022 00:00 23.10.2022 23:59 30.10.2022 23:59



No lecture notes are available.

Previous knowledge

This course builds on the material taught in the VU Formal Methods in Computer Science. Students of this course are supposed to take the VU Formal Methods in Computer Science in parallel.

Accompanying courses