| Abstract |
|
This paper describes 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
stacked while the base VCG is left unchanged. The
technique can be used to build a set of weaker VCGs
to do light weight verification. Moreover, it enables us
to add an ability to generate validation traces. The
paper explains the technique through an example that
extends a simple language L0 with new constructs to
handle exceptions. To deal with exceptions, not only
the logic of L0 has to be extended with new rules, its
structure also needs to be changed. We show that using
our technique the extension can be implemented in
a simple and compositional way, without any change
to the underlying logic.
|
 Additional Information
|
Index Terms- verification tool, verification technique,modular verification
Citation:
I.S.W.B. Prasetya, A. Azurat, T.E.J. Vos, A. Van Leeuwen,
"Building Verification Condition Generators by Compositional Extensions,"
sefm,
pp. 220-230,
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05),
2005
|
