Lab for Automated Reasoning and Analysis LARA

Lecture 03a: From Programs to Formulas

Compositional VCG - Computing Formulas for Loop-Free Commands by Following Program Structure

Forward VCG - Strongest Postconditions rules

Backward VCG - Weakest Preconditions rules

Continued in Lecture 04

 
sav10/lecture_03a.txt · Last modified: 2010/03/09 17:11 by vkuncak
 
© EPFL 2018 - Legal notice