Lab for Automated Reasoning and Analysis LARA

Lecture 04: Generating Formulas from Programs

(Continuing Lecture 03. Review of Homework 03)

Formulas and Relations - Moving from abstract relation representations towards formulas that describe relations

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

Forward VCG - Strongest Postconditions rules

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

(Continuing in Lecture 04a)

 
sav09/lecture_04.txt · Last modified: 2009/03/11 14:53 by vkuncak
 
© EPFL 2018 - Legal notice