School of Electronics and Computer Science
University of Southampton
Thursday, 9 October 2008, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [ppt]
Abstract: Hoare-style 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 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. The explanations can be customized to capture different aspects of the VCs; here, we focus on labelings that explain their structure and purpose. (Joint work with Ewen Denney, USRA/RIACS, NASA Ames Research Center.)