| instruction set simulator with modelling of energy consumtion is Wattch |
instruction set simulator with modelling of energy consumtion is Wattch |
| \cite{BrooksTiwariMartonosi00}. |
\cite{BrooksTiwariMartonosi00}. |
| |
|
| Compiler Verification |
Three aspects of program and compiler correctness exist. The verifying |
| |
compiler proves properties of the translated program and is a grand challenge |
| |
for computing research \cite{Hoare03}. A certified compiler like Verfix is |
| |
proven once to do semantically equivalent optimizations and translations |
| |
\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves |
| |
at every compiler run that the translation is correct and was introduced by |
| |
Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now |
| |
some optimizations have been verified, recently lazy code motion |
| |
\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole |
| |
code generation phase \cite{BlechPoetzsch07}. Another research direction is the |
| |
construction of general frameworks for validation \cite{ZaksPnueli08} or |
| |
generalizations like parameterized equivalence checking \cite{Kundu+09}. |
| |
|
| |
|
| \cite{Hoare03} |
|
| \cite{TristanLeroy09} |
|
| \cite{TristanLeroy08} |
|
| \cite{Kundu+09} |
|
| \cite{Necula00} |
|
| \cite{ZaksPnueli08} |
|
| \cite{Pnueli98a} |
|
| \cite{Pnueli98b} |
|
| \cite{GlesnerGoosZimmeermann04} |
|
| \cite{GoosZimmermann00} |
|
| \cite{BlechPoetzsch07} |
|
| |
|
| WCET \cite{} |
WCET \cite{} |
| |
|
