Graph-based Reduction of Program Verification Conditions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2008

Graph-based Reduction of Program Verification Conditions

Résumé

In the verification of C programs by deductive approaches based on automated provers, some heuristics of separation analysis are proposed to handle the most difficult problems. Unfortunately, these heuristics are not sufficient when applied on industrial C programs: some valid verification conditions cannot be automatically discharged by any automated prover mainly due to their size and a high number of irrelevant hypotheses. This work presents a strategy to reduce program verification conditions by selecting their relevant hypotheses. The relevance of a hypothesis is the combination of separated static dependency analyzes based on graph constructions and traversals. The approach is applied on a benchmark issued from industrial program verification.
Fichier principal
Vignette du fichier
RR-6702.pdf (338.65 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00339847 , version 1 (19-11-2008)

Identifiants

  • HAL Id : inria-00339847 , version 1

Citer

Jean-François Couchot, Alain Giorgetti, Nicolas Stouls. Graph-based Reduction of Program Verification Conditions. [Research Report] RR-6702, INRIA. 2008, pp.22. ⟨inria-00339847⟩
144 Consultations
119 Téléchargements

Partager

Gmail Facebook X LinkedIn More