# 185.291 Formal Methods in Computer Science This course is in all assigned curricula part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});This course is in at least 1 assigned curriculum part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2023W 2023S 2022W 2022S 2021W 2021S 2020W 2020S 2019W 2019S 2018W 2018S 2017W 2017S 2016W 2016S 2015W 2015S 2014W 2014S 2013W 2013S 2012W 2012S 2011W 2011S 2010W 2010S 2009W 2009S 2008W 2008S 2007W 2006W

2023S, VU, 4.0h, 6.0EC

## 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

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`

## Course dates

DayTimeDateLocationDescription
Mon09:00 - 11:0006.03.2023 - 12.06.2023EI 8 Pötzl HS - QUER Q+A Sessions
Tue13:00 - 15:0007.03.2023 - 21.03.2023EI 2 Pichelmayer HS - ETIT Q+A Sessions
Tue13:00 - 15:0018.04.2023 - 20.06.2023EI 2 Pichelmayer HS - ETIT Q+A Sessions
Wed16:00 - 18:0031.05.2023FAV Hörsaal 1 - INF FMI - Certora Talk by Prof. Mooly Sagiv
Formal Methods in Computer Science - Single appointments
DayDateTimeLocationDescription
Mon06.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue07.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon13.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue14.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon20.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue21.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon27.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Mon17.04.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue18.04.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon24.04.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue25.04.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Tue02.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon08.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue09.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon15.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue16.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mon22.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Tue23.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Wed31.05.202316:00 - 18:00FAV Hörsaal 1 - INF FMI - Certora Talk by Prof. Mooly Sagiv
Mon05.06.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions

## Examination modalities

The evaluation is based on a written exam.

## Exams

DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Tue16:00 - 19:0031.10.2023EI 7 Hörsaal - ETIT written09.10.2023 08:00 - 27.10.2023 20:00TISSExam 2 SS
Tue17:00 - 19:0012.12.2023Informatikhörsaal - ARCH-INF written27.11.2023 00:00 - 08.12.2023 23:59TISSExam 3 SS
Tue15:00 - 18:0023.01.2024Informatikhörsaal - ARCH-INF written31.12.2023 00:00 - 19.01.2024 23:59TISSExan 1 WS
Fri13:00 - 16:0015.03.2024Informatikhörsaal - ARCH-INF written27.02.2024 00:00 - 11.03.2024 23:59TISSExam 2 WS
Fri13:00 - 16:0017.05.2024Informatikhörsaal - ARCH-INF written08.04.2024 09:00 - 10.05.2024 23:59TISSExam 3 WS

## Course registration

Begin End Deregistration end
16.02.2023 00:00 26.03.2023 23:59 26.03.2023 23:59

## Literature

For slides end exercises see the TUWEL online course.

English