This is an old revision of the document!

Lecture 3 (Skeleton)

Recall that we can

represent programs using guarded command language, e.g. desugaring of 'if' into non-deterministic choice and assume
give meaning to guarded command language statements as relations
we can represent relations using set comprehensions; if our program has two state components, we can represent its meaning as

$\{((x_0,y_0),(x,y)) \mid F \}$ where F is some formula that mentions x,y,x_0,y_0.

Our goal is to compute this formula.

Verification condition generation in Spec#: http://research.microsoft.com/~leino/papers/krml157.pdf
Loop invariant inference for set algebra formulas: hob-tcs.pdf
Induction-iteration method for machine code checking: http://www.cs.wisc.edu/wpis/papers/pldi00.ps