Explaining Verification Conditions

9 years 4 days ago
Explaining Verification Conditions
The Hoare approach to program verification relies on the construction and discharge of verification conditions (VCs) but offers no support to trace, analyze, and understand the VCs themselves. We describe a systematic extension of the Hoare rules by labels so that the calculus itself can be used to build up explanations of the VCs. The labels are maintained through the different processing steps and rendered as natural language explanations. The explanations can easily be customized and can capture different aspects of the VCs; here, we focus on labelings that explain their structure and purpose. The approach is fully declarative and the generated explanations are based only on an analysis of the labels rather than directly on the logical meaning of the underlying VCs or their proofs.
Ewen Denney, Bernd Fischer 0002
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Authors Ewen Denney, Bernd Fischer 0002
Comments (0)