Lab for Automated Reasoning and Analysis LARA

Lecture 02: From Programs to Relations

(We have seen some motivation in Lecture 01)

Big Picture of VCG - Approach to Verification.

Sets and Relations - Review of Basic Concepts and Notation.

Simple Programming Language - Turing-complete imperative language which we will use to illustrate verification.

Relational Semantics - Specifying meaning of programs using relations, their composition, union and transitive closure.

(Continued in Lecture 03)

 
sav09/lecture_02.txt · Last modified: 2009/03/10 17:59 by vkuncak
 
© EPFL 2018 - Legal notice