VerificationConditionExplanation

To perform software verification a verification condition (VC) must be generated in some fashion. The Mobius PVE contains two primary VC generators (or VCgen for short) in its gamma release. A new VCgen, included in the FreeBoogie subsystem, will be included in a later release.

Verification condition generation is essentially an algorithm that operates upon some input that describes a program, and produces a logical verification condition describes some desired properties of that program. Thus, each VCgen takes some AST as input, and produces some AST as output.

Version: 1 Time: Mon Mar 31 12:47:25 2008 Author: dcochran (dcochran) IP: 193.1.132.32