Diff for /res/PP-compiler.tex between versions 1.8 and 1.9

version 1.8, 2009/06/28 16:26:25 version 1.9, 2009/06/28 16:53:25
Line 70  in the Handbook of Signal Processing sys Line 70  in the Handbook of Signal Processing sys
 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{}
   

Removed from v.1.8  
changed lines
  Added in v.1.9


FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>