Lab for Automated Reasoning and Analysis LARA

Lecture 02: From Programs to Relations

Background: Sets and relations and book chapter

Big Picture of VCG - Approach to Verification.

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.

Using Relational Semantics - Applying Relational Semantics to Prove Program Properties

sav10/lecture_02.txt · Last modified: 2010/03/02 18:46 by vkuncak