Formal methods

Which of these are valid partial-correctness triples over the integers? (Choose all that apply.)

Compute $\mathrm{wp}(y := x + 3;\ z := 2y,\ \; z = 20)$. It has the form $x = n$. What is $n$?

The program $s := 0;\ i := 0;\ \mathtt{while}\ i \lt n\ \mathtt{do}\ (i := i + 1;\ s := s + i)$ should satisfy $\{n \ge 0\}\ \cdot\ \{s = n(n+1)/2\}$. Which loop invariant lets the loop rule and the rule of consequence prove this?

In the soundness proof of Hoare logic, the loop case is proved by induction on the derivation of $\langle \mathtt{while}\ b\ \mathtt{do}\ c, s\rangle \Downarrow t$. Why would structural induction on the command not work?

Which CTL formula says: from every reachable state it is possible to get back to an initial state (a "reset" property)?

A Kripke structure has states $1, \dots, 6$ and transitions $1 \to 2$, $2 \to 3$, $3 \to 3$, $4 \to 5$, $5 \to 4$, $6 \to 1$. The proposition $p$ holds only in state $3$. Compute $\mathsf{EF}\,p$ by the iteration $Z_0 = \emptyset$, $Z_{k+1} = \{3\} \cup \mathrm{pre}(Z_k)$. How many states satisfy $\mathsf{EF}\,p$?

Programs are written in a Turing-complete language. Which of these problems are undecidable? (Choose all that apply.)

Which Lean definition correctly formalises the partial-correctness triple $\{P\}\ c\ \{Q\}$, where BigStep c s t means that c run from s terminates in t?

A compiler comes with a machine-checked proof that, whenever it succeeds, the generated assembly has only behaviours allowed by the source program, according to formal semantics of the source and assembly languages. Which of the following could still lead to a wrongly behaving executable? (Choose all that apply.)

Write find_violation(initial, successors, is_bad) for explicit-state model checking of a safety property. successors(s) returns a list of states and is_bad(s) a boolean. Return a shortest path [initial, ..., bad_state] to a reachable bad state, or None if no reachable state is bad. Your search must terminate on finite systems with cycles.