TU Wien:Formal Methods in Systems Engineering VU (Kovacs)

Daten

Zuordnungen

Masterstudium Logic and Computation	Modul Formal Methods in Systems Engineering * (Gebundenes Wahlfach)
Masterstudium Software Engineering & Internet Computing (veraltet)	Modul Formal Methods in Systems Engineering + (Gebundenes Wahlfach)
Masterstudium Technische Informatik	Modul Formal Methods in Computer Science (Pflichtfach)

Inhalt

noch offen, bitte nicht von TISS/u:find oder Homepage kopieren, sondern aus Studierendensicht beschreiben.

Ablauf

Like in Formal Methods in Computer Science (which this course replaces) there are exercise sheets for every block, which do not count towards the grade. They are not corrected, but sample solutions are presented in the lecture. There is a small project for each block, which are worth 5 points each. The written exam is 80 points, with 20 points for each block. To pass, at least 2 projects need to be completed, and the total points must be $\geq 51$. There are no additional requirements to have certain points in the exam or in every block.

There are 2 exam dates. After the first date, they only issue a certificate for students who passed. If a student passes the first exam they can also take the second, but the latest attempt counts.

Benötigte/Empfehlenswerte Vorkenntnisse

Logic - without knowing first order logic it would be very hard; modal logic is helpful for the Kripke structures used in block 4

Lambda calculus, functional programming is helpful for block 3

Some programming experience for the projects - not necessarily in the languages used, the projects are quite small

Vortrag

noch offen

Übungen

Block 1 Satisfiability

Python - using pySAT to implement a given algorithm

Block 2 Deductive Verification

Dafny - adding annotations to a given program that implements the extended euclidean algorithm

Block 3 Refinement Types

LiquidHaskell - mostly adding refinement types to given functions, but also adding additional functions

Block 4 Model Checking and Temporal Logic

NuSMV - completing a given model and adding LTL specifications

Prüfung, Benotung

noch offen

Dauer der Zeugnisausstellung

noch offen

Zeitaufwand

noch offen

Unterlagen

Block 2 Deductive Verification

Only slight changes to block 3 in the old version, so looking at old exercises and exams is useful: Formal Methods in Computer Science

Block 3 Refinement Types

This youtube series might be helpful for people who have not used Haskell before: Haskell for Imperative Programmers

Lambda calculus playlist, this video includes logical connectives that were asked in the exam on 2026-02-27: https://www.youtube.com/watch?v=K-4Mj3LpP2E

Tipps

noch offen

Highlights / Lob

noch offen

Verbesserungsvorschläge / Kritik

noch offen

Materialien

Neues Material hinzufügen

E

• Exam 2026-01-28

F

• FMSE Block4ExerciseSolution.pdf (details)