TU Wien:Formal Methods in Systems Engineering VU (Kovacs)/Exam 2026-01-28

Block 1

Question 1 (<10 points)

Like exercise 1 - check if clause sets are unsat, sat, refutable, and valid. Write a satisfying assignment or an unsat subset of clauses.

Question 2 (>10 points)

Like exercise 5 - answer questions for a CDCL graph. In addition to giving the resolution derivation and decision level to jump back to, we also had to draw the graph after the jump back and apply BCP.

Block 2

Question 1 (>10 points)

Program:

z:= 0;
while z < y do: 
  x := x + 3 * z + 1;
  y := y - 3 * z - 1;
  z := z + 1;
od

Which of these is valid (give a proof or a counterexample)

$\{x=0\land y=n\land n>0\}p\{x+y=n\}$

$\{x=n\land y=0\land n=0\}p\{x+y=n\}$

$\{x=n\land y=n\land n>0\}p\{x+y=n\}$

Question 2 (<10 points)

For a given program (something simple like y:=x+1;) give non-trivial pre- and postconditions such that {A}p{B} is

• valid
• invalid

and justify your answer. Non-trivial means not just true/false.

Block 3

Question 1 (<10 points)

Like exercise 1 - provide a λ-term that appends one list to another and show that append [x] [y] evaluates to [x,y]

Question 2 (>10 points)

Consider a function map, that applies a function to each element in a given list.

map f l = case l of Nilα => Nilβ; consα (n,t) => consβ (f,h) (map f t)

represent the map function using fixpoint operator and construct a typing derivation witnessing $\vdash map=(\alpha \rightarrow \beta )\rightarrow l:List\alpha \rightarrow \{v:List\beta |lenl=lenv\}$

Block 4

Question 1 (10 points)

Encode the Until operator in past-time LTL

Question 2 (10 points)

For a given past-time LTL formula (something like $once(p\land previously\neg p)$) construct a transition relation $T_{aux}$.