(Continuing Labs 03)

Finishing Forward VCG (Exponentially Sized Formulas and Alternative using Formula for Relation)

Backward VCG - Weakest Preconditions rules as formula transformations, which correspond to Hoare Logic Basics definitions on sets

Syntactic Rules for Hoare Logic - We derive syntactic rules that do not directly refer to semantics of commands as relations.

Forward Symbolic Execution - How to combine program execution and strongest postconditions.

Forward with Hoare - a nice survey paper

(Continued in Exercise 04)