Volume 132, Number 1, May 2005

Proceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)

• 
  Jens Knoop, George C. Necula, Wolf Zimmermann: Preface. 1-3
• 
  Sorin Lerner, Todd D. Millstein, Craig Chambers: Cobalt: A Language for Writing Provably-Sound Compiler Optimizations. 5-17
• 
  Sabine Glesner, Simone Forster, Matthias Jäger: A Program Result Checker for the Lexical Analysis of the GNU C Compiler. 19-35
• 
  Arnd Poetzsch-Heffter, Marek Gawkowski: Towards Proof Generating Compilers. 37-51
• 
  Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett: Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. 53-71
• 
  Sabine Glesner: A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics. 73-93
• 
  Karsten Klohs, Uwe Kastens: Memory Requirements of Java Bytecode Verification on Limited Devices. 95-111
• 
  Elvira Albert, Germán Puebla, Manuel V. Hermenegildo: An Abstract Interpretation-based Approach to Mobile Code Safety. 113-129
• 
  Sid Ahmed Ali Touati: On the Optimality of Register Saturation. 131-148