Lab for Automated Reasoning and Analysis LARA

Generating Verification Conditions

Review: Hoare triples, wp, sp from previous lecture03.

Big Picture of VCG

We will first consider programs without loops.

Normal Form of Loop-Free Programs

Compositional VCG

Forward VCG

Backward VCG

We continue with verification-condition generation in lecture05.

sav08/lecture04.txt · Last modified: 2008/03/04 19:18 by vkuncak