6th International Workshop on
Compiler Optimization Meets Compiler Verification
COCV 2007

Braga, Portugal, 25 March, 2007

In conjunction with the

10th European Joint Conferences on
Theory and Practice of Software
ETAPS 2007

Braga, Portugal
March 24 - April 1, 2007
http://www.di.uminho.pt/etaps07/

Call for Papers: txt pdf

Workshop Description

COCV provides a forum for researchers and practitioners working on optimizing and verifying compilation, and on related fields such as translation validation, certifying compilation and embedded systems with a special emphasis on hardware verification, formal synthesis methods, correctness aspects in HW/SW co-design, formal verification of hardware/software systems, and practical and industrial applications of formal techniques for exchanging their latest findings, and for plumbing the mutual impact of these fields on each other. By encouraging discussions and co-operations across different, yet related fields, the workshop strives for bridging the gap between the communities, and for stimulating synergies and cross-fertilizations among them. Submission of papers at the joint of all these fields is solicited.

Previous COCV workshops have taken place in 2002 in Grenoble, in 2003 in Warsaw, in 2004 in Barcelona, in 2005 in Edinburgh and in 2006 in Vienna, always as a satellite event of the ETAPS conferences. More information can be found at http://www.complang.tuwien.ac.at/cocv2006/cocv2006.html.


Workshop Program


Sunday, March 25, 2007

09:00 - 09:15 Opening: Jens Knoop, Technical University of Vienna
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: Specify, Compile, Run: Hardware from PSL
12:30 - 14:00 Lunch
14:00 - 15:00 Geoff Hamilton: Distilling Programs for Verification
15:00 - 16:00 María del Mar Gallardo, Christophe Joubert and Pedro Merino: 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: Generating Java Compiler Optimizers Using Bidirectional CTL
17:30 - 18:30 Jan Olaf Blech and Arnd Poetzsch-Heffter: A Certifying Code Generation Phase
18:30 Closure

Invited Talk

The invited talk is given by Alan Hu, University of British Columbia, Canada.
Alan Hu received his BS and PhD degrees from Stanford University.  He is a professor of computer science at the University of British Columbia.  For the past 15 years, his main research focus has been automated, practical techniques for formal verification. He has served on the program committees of all major CAD and formal verification conferences, and chaired or co-chaired CAV (1998), HLDVT (2003), and FMCAD (2004). He was also a Technical Working Group Key Contributor on the 2001 International Technology Roadmap for Semiconductors, and is a member of the Technical Advisory Board of Jasper Design Automation.


Title: High-Level vs. RTL Equivalence Checking: Why the Next Big Success of Formal Verification Needs COCV
Abstract: Equivalence checking between combinational circuits is the biggest success story of formal verification, having spawned several successful companies, achieving universal adoption in industry, and completely supplanting the formerly large task of RTL-vs.-Gate-Level simulation. Now, after a quarter century stuck at RTL, hardware design is finally moving to higher-level specifications, creating a pressing need for high-level-vs.-RTL equivalence checking.
In this talk, I will introduce this problem domain and highlight key areas where I believe expertise from the COCV community can play a vital role.

Program Co-Chairs for COCV 2007

Program Committee

Official Address and Organization

For any questions related to COCV 2007 please refer to our web site: or email to: glesner at cs dot tu-berlin dot de

Submission Information and Proceedings

Papers should be submitted electronically in standard Postscript or PDF to Sabine Glesner (glesner at cs dot tu-berlin dot de), together with a plain text message containing the paper's title, author name(s), abstract, and keywords. The format of submissions should adhere to the format of Elsevier's ENTCS Series and should not exceed 15 pages. Submissions that are clearly too long may be rejected immediately. Email addresses and fax numbers of the authors should be included on the title page. Submitted papers must be unpublished and not submitted for publication elsewhere.

As in previous years, the proceedings of accepted papers will be published in the Electronic Notes in Theoretical Computer Science (ENTCS) series, Elsevier Science, Amsterdam, The Netherlands. Preliminary proceedings will be available at the workshop. Selected papers will be considered for publication in a special issue of an appropriate journal. The specific publication venue has not yet been decided on. These submissions will pass through a second round of peer-reviewing.

Summary of Key Dates

Contact: Sabine Glesner (glesner (at) cs.tu-berlin.de) http://pes.cs.tu-berlin.de/

This Workshop has also been anounced by the ARTIST2 Network of Excellence.