Lab for Automated Reasoning and Analysis LARA

Lecture 03: Hoare Logic and Formulas

Remember Relational Semantics

Hoare Logic Basics - Hoare Triple, Strongest Postcondition, Weakest Precondition, Non-deterministic loops


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

Continued in Lecture 03a

sav10/lecture_03.txt · Last modified: 2010/03/09 15:07 by vkuncak
© EPFL 2018 - Legal notice