Brewing Your Own Verification Engine
Stc
Date: 2006-03-30
Time: 11:45
Room: BBL room 471
Title: Brewing Your Own Verification Engine
Abstract
This talk is about how to use some existing technologies to build a Hoare-logic
engine for an imperative language. Rather than providing a Hoare-logic at
the source language's native level, much greater flexibility and
maintainability can be obtained by implementing the logic at an
intermediate level. Furthermore, we will also discuss an implementation of
such an intermediate logic in the theorem prover HOL, and how to play with
it.
Further information:
Rustan Leino et al:
checking Java programs via guarded commands
Obtaining L00:
here
