Lab for Automated Reasoning and Analysis LARA

More on Verification-Condition Generation

Continuing from lecture04, we next look at proof rules for loops, assuming loop invariants are given.

Hoare Logic Rule for Loops

Summary of Hoare Logic

How to combine program execution and strongest postconditions?

Forward Symbolic Execution

We next look at a program semantics that has explicit error conditions, and that gives nice rules for weakest preconditions.

Assert and Error Conditions

Backward VCG With Loops

 
sav08/lecture05.txt · Last modified: 2008/03/06 19:03 by vkuncak
 
© EPFL 2018 - Legal notice