Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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)
Complete list of metadata
Contributor : Alain Giorgetti Connect in order to contact the contributor
Submitted on : Wednesday, November 19, 2008 - 11:04:08 AM
Last modification on : Friday, October 28, 2022 - 3:28:44 AM
Long-term archiving on: : Monday, June 7, 2010 - 11:05:59 PM


Files produced by the author(s)


  • HAL Id : inria-00339847, version 1


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⟩



Record views


Files downloads