Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 05311

Verifying Optimizing Compilers

( Jul 31 – Aug 05, 2005 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



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

  • Andrew W. Appel (Princeton University, US) [dblp]
  • Jan Olaf Blech (KIT - Karlsruher Institut für Technologie, DE)
  • Edsko de Vries (Trinity College Dublin, IE)
  • Gabriel Dos Reis (Texas A&M University - College Station, US)
  • Michael Franz (University of California - Irvine, US) [dblp]
  • Marek Gawkowski (TU Kaiserslautern, DE)
  • Sabine Glesner (TU Berlin, DE) [dblp]
  • Wolfgang Goerigk (Universität Kiel, DE)
  • Benjamin Goldberg (New York University, US)
  • Thomas Hillenbrand (MPI für Informatik - Saarbrücken, DE)
  • Alan Hu (University of British Columbia - Vancouver, CA) [dblp]
  • Thomas In der Rieden (Universität des Saarlandes, DE) [dblp]
  • Tudor Jebelean (Universität Linz, AT)
  • Neil D. Jones (University of Copenhagen, DK) [dblp]
  • Uwe Kastens (Universität Paderborn, DE)
  • Karsten Klohs (Universität Paderborn, DE)
  • Jens Knoop (TU Wien, AT) [dblp]
  • Laura Kovács (Universität Linz, AT) [dblp]
  • Hans Langmaack (Universität Kiel, DE)
  • Sorin Lerner (University of Washington - Seattle, US)
  • Marius Minea (Polytechnical University - Timisoara, RO)
  • Charles Robert Morgan (DataPower Technology - Cambridge, US)
  • Markus Müller-Olm (Universität Münster, DE) [dblp]
  • Iman Narasamdya (University of Manchester, GB)
  • George Necula (University of California - Berkeley, US)
  • Wolfgang J. Paul (Universität des Saarlandes, DE) [dblp]
  • Arnd Poetzsch-Heffter (TU Kaiserslautern, DE) [dblp]
  • Dirk Pollmächer (Martin-Luther-Universität Halle-Wittenberg, DE)
  • Christian W. Probst (Technical University of Denmark - Lyngby, DK) [dblp]
  • Hanan Samet (University of Maryland - College Park, US)
  • Gerhard Schellhorn (Universität Augsburg, DE) [dblp]
  • Bernhard Scholz (The University of Sydney, AU) [dblp]
  • Helmut Seidl (TU München, DE) [dblp]
  • Zhong Shao (Yale University, US) [dblp]
  • K. C. Shashidhar (IMEC - Leuven, BE)
  • Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
  • Wolf Zimmermann (Martin-Luther-Universität Halle-Wittenberg, DE)
  • Lenore D. Zuck (University of Illinois - Chicago, US) [dblp]