Generation of correct, yet highly performant code, are central demands users impose on their compilers. While correctness essentially boils down to semantics preservation between source and target program, performance is typically considered with respect to quite diverse dimensions such as run-time, code size, or power consumption. Though optimizers are integral parts of now-a-days compilers, and research on compiler verification made substantial and impressive progress in the past and is maturing, it is still subject to research how to best combine and reconcile optimizing and verifying compilation, i.e., how to extend the techniques of compiler verification to compiler optimization, or vice versa, to make compiler optimizations more easily amenable to compiler verification. Striving for adequately answering these questions is a constant stimulus for research in compiler optimization and verification, and related fields such as translation validation and certifying and credible compilation, touching also fields such as programming languages design and semantics as lose parts of a language's semantics specification as well as the kind of application ("stand-alone" programs, communicating and reactive systems, etc.) introduce room for interpretation of what semantics preservation really means.
The aim of the workshop is to bring together researchers and practitioners working on optimizing and verifying compilation, and related fields such as optimization validation, certifying and credible compilation, in particular, also for DSLs, programming language design and programming language semantics for exchanging their latest findings, for plumbing the mutual impact of these fields on each other, and for stimulating cross-fertilizations.
Submission of papers at the joint of all these fields is solicited.
This includes (but is not limited to) translation validation,
certifying and credible compilation, profile- and feedback-guided
optimization, and dynamic or just-in-time compilation and
optimization. Particularly welcome are papers on optimization and
verification emphasizing the safety policy imposed on and ensured by
the optimization they are aiming at, how it is established, and how it
can be adapted within the boundaries set up by the overall demand of
correctness and hence semantics preservation.