Programme of COCV at ETAPS 2008

(Compiler Optimization Meets Compiler Verification)

Saturday, April 5, room: Room III.

Welcome and Opening

Jens Knoop

09:15 - 10:30 SESSION 2 (Chair: Jens Knoop)

INVITED TALK

To be announced.

Kurt Wallnau (Carnegie Mellon University, Pittsburgh, PA, USA)

10:30 - 11:00 Coffee

11:00 - 12:30 SESSION 3 (Chair: Sabine Glesner)

Validation I

Validating Correctness of Compiler Optimizer Execution Using Temporal Logic

Masataka Sassa and Soichiro Sahara (Tokyo Institute of Technology, Japan)

Proving Program Properties in Translation Validation

Andrei Voronkov (The University of Manchester, UK) and Iman Narasamdya (Verimag, Grenoble, France)

12:30 - 14:00 Lunch

14:00 - 15:30 SESSION 4 (Chair: Wolf Zimmermann)

Validation II

Validation of Interprocedural Optimizations

Amir Pnueli and Anna Zaks (New York University, NY, USA)

A Summary Function Model for the Validation of Interprocedural Analysis Results

Karsten Klohs (University of Paderborn, Germany)

15:30 - 16:00 Coffee

16:00 - 17:30 SESSION 5 (Chair: Jens Knoop)

Verification and Certification

A Formal Semantics of Intermediate Compiler Representations in Isabelle/HOL

Sabine Glesner and Andreas Humbert (Technical University of Berlin, Germany)

Certifying Code Generation with Coq

Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)

17:30 - 17:50 SESSION 6 (Chair: Wolf Zimmermann)

Tool Demo Session

Certifying Code Generation Runs with Coq: A Tool Description

Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)

17:50 - 18:00 SESSION 7

Closing

Sabine Glesner

Detailed Programme Information:

• Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS
• Workshops: ACCAT, ByteCode, COCV, CMCS, DCC, FESCA, FIT, FORMED, GALOP, GT-VMT, LDTA, MBT, MOMPES, PDMC, QAPL, RV, SafeCert, SC, SLA++P, WGT, WRLA