Lab for Automated Reasoning and Analysis LARA

Program Semantics, Hoare Logic

Simple Programming Language - A 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.

Hoare Logic - Verifying programs by writing sufficient assertions in program code, Weakest Preconditions, Strongest Postconditions.

In lecture04 we will use these notions to express correctness of annotated programs using formulas.

sav08/lecture03.txt · Last modified: 2008/03/02 22:18 by vkuncak