HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Tracing the Origins of Verification Conditions

Ranan Fraer 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The typical program verification system is a batch tool that accepts as input a program annotated with Floyd-Hoare assertions, performs syntactic and semantic analysis on it, and generates a list of verification conditions that is subsequently submitted to a theorem prover. When a verification condition cannot be proved, this may be due to an error in the program or an inconsistency in the annotations. Unfortunately, it is very difficult to relate a failing proof attempt to a particular piece of code or assertion. We propose a solution to this problem using the technique of origin tracking.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073850
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:54:22 PM
Last modification on : Friday, February 4, 2022 - 3:16:24 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:00:07 AM

Identifiers

  • HAL Id : inria-00073850, version 1

Collections

Citation

Ranan Fraer. Tracing the Origins of Verification Conditions. RR-2840, INRIA. 1996. ⟨inria-00073850⟩

Share

Metrics

Record views

20

Files downloads

111