The Community for Technology Leaders
Formal Methods and Models for Co-Design, ACM/IEEE International Conference on (2007)
Nice, France
May 30, 2007 to June 2, 2007
ISBN: 1-4244-1050-9
TABLE OF CONTENTS
Papers

Copyright page (PDF)

pp. ii

Table of Contents (PDF)

pp. iii-iv

Breaker pages (PDF)

pp. nil1

McCharts and Multiclock FSMs for modeling large scale systems (Abstract)

Partha Roop , Department of Electrical and Computer Engineering, University of Auckland, New Zealand
Zoran Salcic , Department of Electrical and Computer Engineering, University of Auckland, New Zealand
Ivan Radojevic , Department of Electrical and Computer Engineering, University of Auckland, New Zealand. email: irad0
pp. 3-12

Design, Implementation, and Validation of a New Class of Interface Circuits for Latency-Insensitive Design (Abstract)

Sampada Sonalkar , Department of Computer Science - Columbia University, City of New York
Rebecca Collins , Department of Computer Science - Columbia University, City of New York
Luca P. Carloni , Department of Computer Science - Columbia University, City of New York
Cheng-Hong Li , Department of Computer Science - Columbia University, City of New York
pp. 13-22

Breaker pages (PDF)

pp. nil2

Formal verification of an optimizing compiler (Abstract)

Xavier Leroy , INRIA Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay, France. Xavier.Leroy@inria.fr
pp. 25

Breaker pages (PDF)

pp. nil3

Computing Invariants for Parameter Abstraction (Abstract)

Hong Pan , State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O.Bo
Yi Lv , State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O.Bo
Huimin Lin , State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O.Bo
pp. 29-38

Executable Analysis using Abstract Interpretation with Circular Linear Progressions (Abstract)

Rathijit Sen , Department of Computer Science and Automation, Indian Institute of Science, Bangalore. E-mail: rathi
Y. N. Srikant , Department of Computer Science and Automation, Indian Institute of Science, Bangalore. E-mail: srika
pp. 39-48

Breaker pages (PDF)

pp. nil4

Scheduling as Rule Composition (Abstract)

Nirav Dave , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
Michael Pellauer , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
null Arvind , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
pp. 51-60

Type Inference for IP Composition (Abstract)

Deepak A. Mathaikutty , Virginia Polytechnic and State University, Blacksburg, VA 24061. mathaikutty@vt.edu
Sandeep K. Shukla , Virginia Polytechnic and State University, Blacksburg, VA 24061. shukla@vt.edu
pp. 61-70

From WiFi to WiMAX: Techniques for High-Level IP Reuse across Different OFDM Protocols (Abstract)

Nirav Dave , Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology. Emai
Muralidaran Vijayaraghavan , Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology. Emai
Gopal Raghavan , Nokia Research Center Cambridge, Nokia Corporation. Email: gopal.raghavan@nokia.com
null Arvind , Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology. Emai
Man Cheuk Ng , Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology. Emai
Jamey Hicks , Nokia Research Center Cambridge, Nokia Corporation. Email: jamey.hicks@nokia.com
pp. 71-80

Breaker pages (PDF)

pp. nil5

Local Causal Reasoning of a Safety-Critical Subway System (Abstract)

Sandeep Shukla , Department of Electrical&Computer Engineering, Whittemore (0111), Offices 332&341, Virginia
Edgar G. Daylight , Department of Electrical&Computer Engineering, Whittemore (0111), Offices 332&341, Virginia
pp. 83-84

Multi-Level Assertion-Based Design (Abstract)

Martin Braun , Computer Systems Group, Darmstadt University of Technology, Germany
Martin Schweikert , Computer Systems Group, Darmstadt University of Technology, Germany
Volker Nimbler , Computer Systems Group, Darmstadt University of Technology, Germany
Hans Eveking , Computer Systems Group, Darmstadt University of Technology, Germany
Martin Schickel , Computer Systems Group, Darmstadt University of Technology, Germany
pp. 85-86

Extended Architecture Analysis Description Language for Software Product Line Approach in Embedded Systems (Abstract)

Youngseok Oh , SOftware Technology Institute, Information and Communications University, Korea. youngseok.oh@icu.ac
Sungwon Kang , SOftware Technology Institute, Information and Communications University, Korea. kangsw@icu.ac.kr
Dan Hyung Lee , SOftware Technology Institute, Information and Communications University, Korea. danlee@icu.ac.kr
Ji Hyun Lee , SOftware Technology Institute, Information and Communications University, Korea. puduli@icu.ac.kr
pp. 87-88

Breaker pages (PDF)

pp. nil6

MEMOCODE 2007 Co-Design Contest (Abstract)

Forrest Brewer , ECE Dept. UC Santa Barbara. forrest@ece.ucsb.edu
James C. Hoe , ECE Dept. Carnegie Mellon University. jhoe@ece.cmu.edu
pp. 91-94

VT Matrix Multiply Design for MEMOCODE '07 (Abstract)

Sandeep Shukla , Virginia Tech, Electrical and Computer Engineering Deptartment, Blacksburg, VA 24060. shukla@vt.edu
Sumit Ahuja , Virginia Tech, Electrical and Computer Engineering Deptartment, Blacksburg, VA 24060. sahuja@vt.edu
Eric Simpson , Virginia Tech, Electrical and Computer Engineering Deptartment, Blacksburg, VA 24060. esimpson@vt.ed
Pengyuan Yu , Virginia Tech, Electrical and Computer Engineering Deptartment, Blacksburg, VA 24060. peyu1983@vt.ed
Patrick Schaumont , Virginia Tech, Electrical and Computer Engineering Deptartment, Blacksburg, VA 24060. schaum@vt.edu
pp. 95-96

Hardware Acceleration of Matrix Multiplication on a Xilinx FPGA (Abstract)

Kermin Fleming , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
Myron King , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
Nirav Dave , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
Michael Pellauer , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
Muralidaran Vijayaraghavan , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge,
pp. 97-100

Breaker pages (PDF)

pp. nil7

Towards a Unified Execution Model for Transactions in TLM (Abstract)

Christian Haubelt , University of Erlangen-Nuremberg, Erlangen, Germany. haubelt@cs.fau.de
Bernhard Niemann , Fraunhofer Institute for Integrated Circuits, Erlangen, Germany. bernhard.niemann@iis.fraunhofer.de
pp. 103-112

Towards Equivalence Checking Between TLM and RTL Models (Abstract)

Franco Fummi , Dipartimento di Informatica, Universit? di Verona, Italy. fummi@sci.univr.it
Joao Marques-Silva , School of Electronics and Computer Science, University of Southampton, UK. jpms@ecs.soton.ac.uk
Nicola Bombieri , Dipartimento di Informatica, Universit? di Verona, Italy. bombieri@sci.univr.it
Graziano Pravadelli , Dipartimento di Informatica, Universit? di Verona, Italy. pravadelli@sci.univr.it
pp. 113-122

Verification Driven Formal Architecture and Microarchitecture Modeling (Abstract)

Carven Chan , Department of EE, Princeton University, Princeton, NJ 08544, USA. carvenc@princeton.edu
Yogesh Mahajan , Department of EE, Princeton University, Princeton, NJ 08544, USA. yogism@princeton.edu
Ali Bayazit , Department of EE, Princeton University, Princeton, NJ 08544, USA. abayazit@princeton.edu
Sharad Malik , Department of EE, Princeton University, Princeton, NJ 08544, USA. sharad@princeton.edu
Wei Qin , ECE Department, Boston University, Boston, MA 02215, USA. wqin@bu.edu
pp. 123-132

Breaker pages (PDF)

pp. nil8

Proving What Programs Do Not (Abstract)

Bertrand Meyer , ETH, Zurich, Eiffel Software, Santa Barbara
pp. 135

Breaker pages (PDF)

pp. nil9

Software/Hardware Engineering with the Parallel Object-Oriented Specification Language (Abstract)

J. Huang , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
M.C.W. Geilen , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
O. Florescu , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
B.D. Theelen , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
J.P.M. Voeten , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
P.H.A. van der Putten , Eindhoven University of Technology, Department of Electrical Engineering, P.O. Box 513, 5600 MB Eind
pp. 139-148

One-dimensional Search Algorithms for Hardware/Software Partitioning (Abstract)

Wu Jigang , Centre for High Performance Embedded Systems, School of Computing Engineering, Nanyang Technological
Guang Chen , Centre for High Performance Embedded Systems, School of Computing Engineering, Nanyang Technological
Thambipillai Srikanthan , Senior Member, IEEE, Centre for High Performance Embedded Systems, School of Computing Engineering,
pp. 149-158

A Methodology for Automating Co-Scheduling for Reconfigurable Computing Systems (Abstract)

Proshanta Saha , The George Washington University. sahpa@gwu.edu
Tarek El-Ghazawi , The George Washington University. tarek@gwu.edu
pp. 159-168

Breaker pages (PDF)

pp. nil10

Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols (Abstract)

Geoffrey M. Brown , Indiana University, Bloomington. geobrown@cs.indiana.edu
null Lee Pike , Galois, Inc. leepike@galois.com
pp. 171-180

Combining Multi-Valued Logics in SAT-based ATPG for Path Delay Faults (Abstract)

Stephan Eggersgluess , Institute of Computer Science, University of Bremen, 28359 Bremen, Germany. segg@informatik.uni-brem
Friedrich Hapke , NXP Semiconductors Germany GmbH, 21147 Hamburg, Germany. friedrich.hapke@nxp.com
Andreas Glowatz , NXP Semiconductors Germany GmbH, 21147 Hamburg, Germany. andreas.glowatz@nxp.com
Rolf Drechsler , Institute of Computer Science, University of Bremen, 28359 Bremen, Germany. drechsle@informatik.uni-
Juergen Schloeffel , NXP Semiconductors Germany GmbH, 21147 Hamburg, Germany. juergen.schloeffel@nxp.com
Gorschwin Fey , Institute of Computer Science, University of Bremen, 28359 Bremen, Germany. fey@informatik.uni-breme
pp. 181-187

Easier and More Informative Vacuity Checks (Abstract)

Hana Chockler , IBM Research Mount Carmel, Haifa 31905, Israel. hanac@il.ibm.com
Ofer Strichman , Information Systems Engineering, IE, Technion, Haifa 32000, Israel. ofers@ie.technion.ac.il
pp. 189-198

Breaker pages (PDF)

pp. nil11

Author Index (PDF)

pp. 203
109 ms
(Ver )