Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2007) May 30 - June 1st,  Nice, France

CONFERENCE PROGRAM

Wed, May 30th

8:30 Registration start

9:00 Welcome Opening

9:15-10:15 Timed Models of Computation   
(chair R. de Simone)

• McCharts and Multiclock FSMs for modeling large scale systems - Ivan Radojevic, Zoran Salcic, Partha Roop (University of Auckland)
• Design, Implementation, and Validation of a New Class of Interface Circuits for Latency-Insensitive Design - Cheng-Hong Li, Rebecca Collins, Sampada Sonalkar, Luca Carloni (Columbia University)

10:15 Coffee break & refreshments

10:30 Keynote Address
(chair J-P. Talpin)

• Formal verification of an optimizing compiler - Xavier Leroy (INRIA) - slides available

13:30-14:30 Abstraction and Analysis
(chair J. Hoe)

• Computing Invariants for Parameter Abstraction -Yi Lv, Huimin Lin, Hong Pan (Chinese Academy of Sciences)
• Executable Analysis using Abstract Interpretation with Circular Linear Progressions - Rathijit Sen, Y. N. Srikant (Indian Institute of Science)

15:00-16:30 System Synthesis/Design
(chair S. Devadas)

• Scheduling as Rule Composition - Nirav Dave, Arvind, Michael Pellauer (MIT)
• Type Inference for IP Composition - Deepak Mathaikutty, Sandeep Shukla (Virginia Tech)
• From Wi-Fi to WiMAX: Techniques for IP Reuse across Different OFDM Protocols - Alfred Man Cheuk Ng (MIT), Muralidaran Vijayaraghavan (MIT), Nirav Dave (MIT), Gopal Raghavan (Nokia), Jamey Hicks (Nokia), Arvind (MIT)

17:00-17:15 Poster session presentation
(chair S. Devadas)

• Local Causal Reasoning of a Safety-Critical Subway System - Edgar Daylight, Sandeep Shukla (Virginia Tech)
• Multi-Level Assertion-Based Design - Hans Eveking, Martin Braun, Martin Schickel, Martin Schweikert, Volker Nimbler (Darmstadt University of Technology)
• Extended Architecture Analysis Description Language for Software Product Line Approach in Embedded Systems - Youngseok Oh, Dan Hyung Lee, Sungwon Kang, Ji Hyun Lee (Information and Communications University, Korea)

17:30-19:00 Design Contest results and winner election
(chair Forrest Brewer)

19:00 Welcome Party

Thur, May 31st

9:00- 10:30  Comparing Modeling Levels:
(chair S. Shukla)

• Towards a Unified Execution Model for Transactions in TLM - Bernhard Niemann (Fraunhofer Institute for Integrated Circuits) Christian Haubelt (University of Erlangen-Nuremberg)
• Towards Equivalence Checking Between TLM and RTL Models - Nicola Bombieri (Universita' di Verona), Franco Fummi (Universita' di Verona), Joao Marques-Silva (University of Southampton), Graziano Pravadelli (Universita' di Verona)
• Bridging the "Verification Gap"  through Formal Architecture and Microarchitecture Modeling - Yogesh S. Mahajan, Carven Chan, Alphan Bayazit, Sharad Malik (Princeton University), Wei Qin (Boston University)

11:00 Keynote Address
(chair J. Hoe)

• Proving What Programs Do Not,   Bertrand Meyer (ETH Zurich)

12:30-13:00 Lunch

13:30-15:00 HW/SW Codesign
(chair  R. Gupta)

• Software/Hardware Engineering with the Parallel Object-Oriented Specification Language - B.D. Theelen, O. Florescu, M.C.W. Geilen, J. Huang, P.H.A. van der Putten, J.P.M. Voeten (Eindhoven University of Technology)
• One-dimensional Search Algorithms for Hardware/Software Partitioning - Wu Jigang, Thambipillai Srikanthan, Guang Chen (Nanyang Technological University)
• A Methodology for Automating Co-Scheduling for Reconfigurable Computing Systems - Proshanta Saha, Tarek El-Ghazawi (The George Washington University)

15:00 Coffee break & refreshments

15:30-17:00 Timing Issues & Symbolic techniques
(chair K. Schneider)

• Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols - Geoffrey M. Brown (Indiana University), Lee Pike (Galois, Inc.)
• SAT-based ATPG for Path Delay Faults in Industrial Circuits - Stephan Eggersglüß, Görschwin Fey, Rolf Drechsler (University of Bremen) Andreas Glowatz, Friedrich Hapke, Juergen Schloeffel (NXP Semiconductors Germany GmbH)
• Easier and More Informative Vacuity Checks - Hana Chockler (IBM Haifa Research Lab) Ofer Strichman (Technion Israel Inst. of Technology)

20:00 Banquet at Hotel Boscolo Plaza

Fri, June 1st

• Performance Modelling in Software/Hardware Engineering - Bart Theelen, M.C.W. Geilen, J.P.M. Voeten (Eindhoven University of Technology)

10:30 Coffee Break intermission

12:30-13:30 Lunch

13:30 Keynote Address
(chair K. Schneider)

• Bringing Hardware and Software Closer Together with Termination Analysis, Byron Cook (MicroSoft Research),
  

15:00-18:30 Afternoon tutorial
(chair R. Gupta)

• The CoQ proof assistant - Yves Bertot and Pierre Casteran