# 185.A93 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"});}); 2024W 2023W 2022W 2021W 2020W 2019W 2018W 2017W

2023W, UE, 2.0h, 3.0EC

## Properties

• Semester hours: 2.0
• Credits: 3.0
• Type: UE Exercise
• 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

Immanent

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

## Course dates

DayTimeDateLocationDescription
Fri11:00 - 13:0020.10.2023 - 19.01.2024EI 5 Hochenegg HS FMI UE
Formal Methods in Computer Science - Single appointments
DayDateTimeLocationDescription
Fri20.10.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri27.10.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri03.11.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri10.11.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri17.11.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri24.11.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri01.12.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri15.12.202311:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri12.01.202411:00 - 13:00EI 5 Hochenegg HS FMI UE
Fri19.01.202411:00 - 13:00EI 5 Hochenegg HS 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
01.10.2023 00:00 22.10.2023 23:59 29.10.2023 23:59

## Literature

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.

English