Graph-based Reduction of Program Verification Conditions

Jean-François Couchot 1 Alain Giorgetti 1, 2 Nicolas Stouls 3
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Document type :
Reports
[Research Report] RR-6702, INRIA. 2008, pp.22
Liste complète des métadonnées

https://hal.inria.fr/inria-00339847
Contributor : Alain Giorgetti <>
Submitted on : Wednesday, November 19, 2008 - 11:04:08 AM
Last modification on : Thursday, February 9, 2017 - 3:53:36 PM
Document(s) archivé(s) le : Monday, June 7, 2010 - 11:05:59 PM

File

RR-6702.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00339847, version 1

Citation

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>

Share

Metrics

Record views

267

Document downloads

139