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.

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.

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.

 *********Distance Learning*************
Due to the COVID-19 crisis, this course will be held on-line using the TUWEL platform. Students will receive videos of lectures on all topics of the course. The lectures will be discussed in Q+A Session (2 per block) via Zoom. Exercises will be managed using TUWEL. Solution to the exercises will be presented in Q+A Session (1 per block) via Zoom.

A discussion forum on TUWEL will be used to answer student questions and to clarify issues.

Examination form: Online written exam via TUWEL. The examiners and the students are permanently connected via  audio and video in a online meeting. Solutions can be provided directly to TUWEL or scanned and uploaded by the student within the time specified by the examiner (approx. 5 minutes).

******************************************

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

The evaluation is based on a written exam.

For slides end exercises see the TUWEL online course.