Graph Based Reduction of Program Verification Conditions

Jean-François Couchot 1 Alain Giorgetti 1 Nicolas Stouls 2
1 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
2 AMAZONES - Ambient Middleware Architectures: Service-Oriented, Networked, Efficient and Secured
Inria Grenoble - Rhône-Alpes, CITI - CITI Centre of Innovation in Telecommunications and Integration of services
Abstract : Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is 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 determined by the combination of a syntactic analysis and two graph traversals. The first graph is labeled by constants and the second one by the predicates in the axioms. The approach is applied on a benchmark arising in industrial program verification.
Type de document :
Communication dans un congrès
Hassen Saïdi and N. Shankar. Automated Formal Methods (AFM'09), colocated with CAV'09, Jun 2009, Grenoble, France. ACM Press, pp.40--47, 2009
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00402204
Contributeur : Nicolas Stouls <>
Soumis le : mardi 7 juillet 2009 - 08:37:06
Dernière modification le : mercredi 28 février 2018 - 15:20:15
Document(s) archivé(s) le : mardi 15 juin 2010 - 19:34:42

Fichiers

afm09cgs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00402204, version 1
  • ARXIV : 0907.1357

Collections

INRIA | UNIV-FCOMTE | INSA-LYON | TDS-MACS | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA | UNIV-LORRAINE

Citation

Jean-François Couchot, Alain Giorgetti, Nicolas Stouls. Graph Based Reduction of Program Verification Conditions. Hassen Saïdi and N. Shankar. Automated Formal Methods (AFM'09), colocated with CAV'09, Jun 2009, Grenoble, France. ACM Press, pp.40--47, 2009. 〈inria-00402204〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

317

Téléchargements de fichiers

181

Contact


archive-ouverte@inria.fr