There is a growing awareness, both in industry and academia, of the crucial role of formally proving the correctness of systems. Most verification methods focus on the verification of a specification with respect to a set of requirements, or of high-level code with respect to a specification. However, if one is to prove that a high-level specification is correctly implemented in low-level code, one must verify the compiler which performs the translations. Verifying the correctness of modern optimizing compilers is challenging because of the complexity and reconfigurability of the target architectures, as well as the sophisticated analysis and optimization algorithms used in the compilers.

The introduction of new families of microprocessor architectures, such as the EPIC family exemplified by the Intel IA-64 architecture, places an even heavier responsibility on optimizing compilers. Static compile-time dependence analysis and instruction scheduling are required to exploit instruction-level parallelism in order to compete with other architectures, such as the super-scalar class of machines where the hardware determines dependences and reorders instructions at run-time. As a result, a new family of sophisticated optimizations have been developed and incorporated into compilers targeted at EPIC architectures.

The increasing popularity of embedded systems brings with it a demand for fully automatic certifiers for a wide range of compilers, ensuring an extremely high level of confidence in the compiler in areas, such as safety-critical systems and compilation into silicon, where correctness is of paramount concern. Consequently, we have witnessed, in the past few years, a surge in application of formal method to the development and verification of optimizing compilers.

The goal of the seminar is to bring together researchers in all areas concerning the development of correct and verifiable state-of-the-art compilers compiler, and provide a forum in which they can discuss, study, and develop cooperation, and advance the knowledge in all issues concerning development of verifiable optimizing compilers. By encouraging discussions and cooperations across different, yet related fields, the seminar strives for bridging the gap between the communities, and for stimulating synergies and cross-fertilizations among them. The seminar is a consequence of the recent COCV workshops that are help under ETAPS, the idea of which was conceived in a Dagstuhl seminar (00381) in 2000.

Typical topics of interest include: Translation Validation, Self-Certifying compilers, Verification of Optimizations, Design of verifiable optimizations, Verification of Compilation, Use of logic in designing optimizations, and Impact of verification on compilerconstruction