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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-00848703
Contributor : Sandrine Blazy <>
Submitted on : Sunday, July 28, 2013 - 8:10:56 AM
Last modification on : Thursday, November 15, 2018 - 11:57:41 AM
Document(s) archivé(s) le : Wednesday, April 5, 2017 - 5:17:04 PM

Files

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00848703, version 1

Citation

Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303. ⟨hal-00848703⟩

Share

Metrics

Record views

1158

Files downloads

257