While programs

Fact. Every while program can be simulated by a while program with at most one while loop.

Harel's proof using structural induction
Kozen's proof using KAT
Kleene Algebra with Tests (KAT)
Kozen's lecture notes on KAT
Kozen's result about the complexity & decidability of KAT

CTL vs LTL

• Syntax. A quantifier in a CTL formula are in form of a path quantifier $A,E$ following by a state quantifier $F,X,G,U,W$. A quantifier in an LTL is a combination of state quantifiers.
• States and paths. A CTL formula $\phi$ is a state formula, meaning that the temporal operators are state-based in structure: the derivation of a given formula is per-state and depends on the derivation of subformulas for subsequent states. For example, computing the set of states satisfying $AG\ φ$ relies on computing the set of states satisfying $φ$.
  In contrast, LTL formula $\psi$ is a path formula: the derivation of a given formula depends on the derivation of subformulas for suffixes of a path.
• Entailments. We write $M,s \models \phi$ and $M,p \models \psi$ for state $s$ and path $p$. Given a set $I$ of the initial states of $M$, we shall write $M ⊨ φ$ if $M, s ⊨ φ$ for all $s ∈ I$, and write $M ⊨ ψ$ if $M, s ⊨ ψ$ for all paths starting from $I$.
• LTL and CTL are incomparable. The reset property $AG (EF\ φ)$ (i.e. there is always a possibility that $\phi$ could hold, though it may never hold) cannot be expressed in LTL. The stability property $FG\ φ$ cannot be expressed in CTL.
• Structure vs traces. CTL can characterize the structure while LTL only characterizes the traces. Consider the following two systems:
  $A:$ $(s_1,s_2),\ (s_1,s_3),\ (s_2,s_4),\ (s_3,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  $B:$ $(s_1,s_2),\ (s_2,s_4),\ (s_2,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  where $L(s_1)=a,\ L(s_2)=L(s_3)=b,\ L(s_4)=c,\ L(s_5)=d$. Both systems have traces $(ab(c+d))^\omega$ and thus cannot be distinguished in LTL. On the other hand, $B$ is a model of $AG(b\Rightarrow EX\ c)$ while $A$ isn't.
• There is a lot of discussion of the best logic to express properties for software verification. LTL can express important properties for software system modelling (e.g. fairness) when the CTL must have a new semantics to express them. But CTL algorithms are usually more efficient and can use BDD-based algorithms.

References

1. Making prophecies with decision predicates
2. Branching vs. Linear Time: Final Showdown

Selected Topics in Design & Verification

Model Checking and Synthesis with SMT

1. Verifying system against LTL spec → checking emptiness for NBW → finding bad lassos in run graph → checking existence of ranking functions → SMT model checking
2. Synthesizing system from LTL spec → using UF to represent transition relation and iterating through the possible numbers of states ($\le ~|B|^{|B|}$) → SMT model checking
3. In 1989, Pnueli and Rosner solved the LTL synthesis problem (2EXPTIME-complete): LTL $\phi$ → NBW (~ $2^{|\phi|}$) → DPW (~ $2^{|\phi|^{|\phi|}}$) → solve the game (~ $2^{|\phi|^{|\phi|}}$)

(DPW: deterministic parity word automata; NBW: nondeterministic Buchi word automata)

Dafny resources

Online verifier and tutorial
Using Dafny in Visual Studio

Overviews

1. Getting Started with Dafny (with language reference); a shorter html version.
2. Using Dafny, an Automatic Program Verifier (slide)
3. Dafny: An Automatic Program Verifier for Functional Correctness

4. Dafny: Statically Verifying Functional Correctness.
5. Type system of Dafny / Proving theorems with Dafny.

Lecture notes

Verified programming in Dafny

Forums & blogs

Dafny questions on StackOverflow / The official Dafny forum / Lexical scope

Advanced topics

Non-determinism
Data refinement
Calculational proof
Triggers

Loop invariant resources

Synthesis

Inferring loop invariants using post-conditions:
http://se.ethz.ch/~meyer/publications/proofs/invariant_inference.pdf

Generating loop invariants using predicate abstraction
https://hal.inria.fr/inria-00615623/document

Boogie uses abstract interpretation to infer loop invariants:
http://research.microsoft.com/en-us/um/people/leino/papers/krml160.pdf

Tools

Boogie overview slide
http://webcourse.cs.technion.ac.il/236800/Winter2010-2011/ho/WCFiles/Boogie.pdf

The Z3 SMT solver

Z3 is a Satisfiability Modulo Theories (SMT) solver. It is an automated satisfiability checker for many-typed first-order logic with built-in theories, including support for quantifiers. The currently supported theories are:

• equality over free (aka uninterpreted) function and predicate symbols
• real and integer arithmetic
• bit-vectors and arrays
• tuple/records/enumeration types and algebraic (recursive) data-types.

Z3 checks whether a set of formulas is satisfiable in the built-in theories. When the set of formulas is existential then Z3 is a decision procedure: it is always guaranteed to return a correct answer.

• If a set of formulas F is satisfiable, Z3 can produce a model for F.
• If a set of formulas contains universal quantifiers, then the model produced by Z3 should be viewed as a potential model, since Z3 is incomplete in this case.