Lab for Automated Reasoning and Analysis LARA

Lecture 04: Hoare Logic Rules. Symbolic Execution. Idea of Data-Flow Analysis

Recall Lecture 03a

Syntactic Rules for Hoare Logic - We derive syntactic rules that do not directly refer to semantics of commands as relations.

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

A glimpse of data-flow analysis:

 
sav10/lecture_04.txt · Last modified: 2010/03/19 13:59 by vkuncak
 
© EPFL 2018 - Legal notice