Formal Verification of Loop Bound Estimation for WCET Analysis

Sandrine Blazy 1 André Maroneze 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Worst-case execution time (WCET) estimation tools are complex pieces of software performing tasks such as computation on control flow graphs (CFGs) and bound calculation. In this paper, we present a formal verification (in Coq) of a loop bound estimation. It relies on program slicing and bound calculation. The work has been integrated into the CompCert verified C compiler. Our verified analyses directly operate on non-structured CFGs. We extend the CompCert RTL intermediate language with a notion of loop nesting (a.k.a. weak topological ordering on CFGs) that is useful for reasoning on CFGs. The automatic extraction of our loop bound estimation into OCaml yields a program with competitive results, obtained from experiments on a reference benchmark for WCET bound estimation tools.
Type de document :
Communication dans un congrès
Ernie Cohen and Andrey Rybalchenko. VSTTE - Verified Software: Theories, Tools and Experiments, May 2013, Menlo Park, United States. Springer, 8164, pp.281-303, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00848703
Contributeur : Sandrine Blazy <>
Soumis le : dimanche 28 juillet 2013 - 08:10:56
Dernière modification le : mercredi 11 avril 2018 - 02:01:30
Document(s) archivé(s) le : mercredi 5 avril 2017 - 17:17:04

Fichiers

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

Identifiants

  • HAL Id : hal-00848703, version 1

Citation

Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. Ernie Cohen and Andrey Rybalchenko. VSTTE - Verified Software: Theories, Tools and Experiments, May 2013, Menlo Park, United States. Springer, 8164, pp.281-303, 2013, Lecture Notes in Computer Science. 〈hal-00848703〉

Partager

Métriques

Consultations de la notice

851

Téléchargements de fichiers

219