Programme of COCV at ETAPS 2007

(Compiler Optimization meets Compiler Verification)

Sunday, March 25, room: CP2-108

09:00 - 10:30 SESSION 1

Opening

Jens Knoop, Vienna University of Technology

Invited Talk

High-Level vs. RTL Equivalence Checking: Why the Next Big Success of Formal Verification Needs COCV

Alan Hu, University of British Columbia, Canada

10:30 - 11:00 Coffee Break

11:00 - 12:00 SESSION 2

Specify, Compile, Run: Hardware from PSL

Bloem, Galler, Jobstmann, Piterman, Pnueli, Weiglhofer (Graz University of Technology, Austria; EPFL Lausanne, Switzerland; Weizmann Institute, Israel)

12:30 - 14:00 Lunch

14:00 - 16:00 SESSION 3

Distilling Programs for Verification

Geoff Hamilton (Dublin City University, Ireland)

On-the-Fly Data Flow Analysis based on Verification Technology

MarÌa del Mar Gallardo, Christophe Joubert and Pedro Merino (University of Málaga, Spain)

16:00 - 16:30 Coffee Break

16:30 - 18:00 SESSION 4

Generating Java Compiler Optimizers Using Bidirectional CTL

Ling Fang and Masataka Sassa (Tokyo Institute of Technology, Japan)

A Certifying Code Generation Phase

Jan Olaf Blech and Arnd Poetzsch-Heffter (University of Kaiserslautern, Germany)

16:30 - 18:00 Closure

18:45 SOCIAL EVENT

Joint Workshops Pre-Conference Dinner (tickets needed)

Dinner at Bom Jesus, Braga

Shuttle departure from University Campus, Gualtar

Further ETAPS 2007 Programme Information:

• Programme Overview, Social Programme
• Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS
• Workshops: ACCAT, Bytecode, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS
• Tutorials: Stratego/XT, SoftwGen, Mobius