COCV 2007
Compiler Optimization meets Compiler Verification

Satellite Event of ETAPS 2007
Braga, Portugal
Sunday, March 25, 2007

Organizers: 
Sabine Glesner (Technical University of Berlin, Germany)
Jens Knoop (Vienna University of Technology, Austria)
Rolf Drechsler (University of Bremen, Germany)


09:00 - 09:15: Opening: Jens Knoop, Vienna University of Technology

09:15 - 10:30: Invited Talk: Alan Hu, University of British Columbia, 
Canada: High-Level vs. RTL Equivalence Checking: Why the Next Big 
Success of Formal Verification Needs COCV

10:30 - 11:00: Coffee Break

11:00 - 12:00: Bloem, Galler, Jobstmann, Piterman, Pnueli, Weiglhofer 
(Graz University of Technology, Austria; EPFL Lausanne, Switzerland; 
Weizmann Institute, Israel): 
Specify, Compile, Run: Hardware from PSL

12:30 - 14:00: Lunch

14:00 - 15:00: Geoff Hamilton (Dublin City University, Ireland): 
Distilling Programs for Verification 

15:00 - 16:00: María del Mar Gallardo, Christophe Joubert and 
Pedro Merino (University of Málaga, Spain): 
On-the-Fly Data Flow Analysis based on Verification Technology

16:00 - 16:30 : Coffee Break

16:30 - 17:30: Ling Fang and Masataka Sassa (Tokyo Institute 
of Technology, Japan): 
Generating Java Compiler Optimizers Using Bidirectional CTL

17:30 - 18:30: Jan Olaf Blech and Arnd Poetzsch-Heffter 
(University of Kaiserslautern, Germany): 
A Certifying Code Generation Phase

18:30 Closure