salle A. Turing CE4
6 décembre 2012 - 14h00
Semantics-Based WCET Analysis
par Mihail Asavoae de University Alexandru Ioan Cuza, Iasi, Romania
Abstract: We propose a general methodology for worst-case execution time (WCET) analysis centered around a formal executable semantics of the underlying programming language. We assert that a formal definition of a language has all the necessary information to be used for program analysis and verification, therefore we define, in a rewrite-based framework called K, a formal executable semantics of a MIPS-based assembly language. This definition together with parametric specifications of micro-architecture
