Building Verification Condition Generators By Compositional Extensions
Stc
Date: 2005-09-29
Time: 11:45
Room: BBL room 471
Title: Building Verification Condition Generators by Compositional Extensions
Abstract
In this talk we present a technique that combines algebraic datatypes and
monads to build derivative verification condition generators (VCGs) by
extending a base VCG. Extensions are compositional and can be added in
arbitrary order without modifying the base VCG. We show how we achieve this
result by extending a simple language $L_0$ with a construct for exception
handling.
