Monday, July 11

TUTORIALS

• Sequential equivalence checking
  A. Mathur, M. Fujita, A. Fideli

• Using Esterel for System-Level Design
  S. A. Edwards and S. Singh

Tuesday, July 12

Formal Methods and Models for Codesign (MEMOCODE’2005)

08:45 - 09:00

• Program Chairs Welcome: Connie Heitmeyer, NRL, and John O’Leary, Intel

09:00 - 10:00

• Keynote Talk I

Chair: Constance Heitmeyer, Naval Research Laboratory
Title: A Synchronous Language at Work: The Story of LUSTRE
Keynote Speaker: Nicholas Halbwachs, Verimag

10:00 - 11:00

• Session 1: Hardware Synthesis

Chair: Stephen Edwards, Columbia University

Synthesis of Synchronous Assertions with Guarded Atomic Actions
Michael Pellauer, Massachusetts Institute of Technology Mieszko Lis, Don Baltus, and Rishiyur Nikhil, Bluespec

Automatic Synthesis of Cache-Coherence Protocol Engines Using Bluespec
Nirav Dave, Man Cheuk Ng, and Arvind, Massachusetts Institute of Technology

11:00 - 11:30

• Coffee Break

11:30 - 13:00

• Session 2: Hardware Languages and Semantics

Chair: Masahiro Fujita, University of Tokyo

Deterministic Receptive Processes are Kahn Processes
Stephen A. Edwards, Olivier Tardieu, Columbia University

Structural Operational Semantics for Supporting Multi-Cycle Operations in RTL HDLs
Shuqing Zhao, Daniel Gajski, University of California, Irvine

PyPBS Design and Methodology
Greg Hoover, Forrest Brewer, University of California, Santa Barbara

13:30 - 15:00

• Lunch

15:00 - 16:00

• Invited Tutorial

Chair: Sandeep Shukla, Virginia Tech
Title: Making PVS Do What You Want
Presenter: Myla Archer, Naval Research Laboratory

16:00 - 16:30

• Coffee Break

16:30 - 18:00

• Posters/Work-in-Progress Session

Chair: Arvind, Massachusetts Institute of Technology

Property-Based Verification in SoC Design Flow
Nicola Bombieri, Andrea Fedeli, ST Microelectronics, and Franco Fummi, University of Verona

A Formal Approach from Software Oriented UML Descriptions to Hardware Oriented RTL
Masahiro Fujita, University of Tokyo

Formal Verification of Architectural Patterns in Support of Dependable Distributed Systems
Ralph Jeffords and Ramesh Bharadwaj, Naval Research Laboratory

Organizing Automaton Specifications to Achieve Faithful Representations
Elizabeth I. Leonard and Myla Archer, Naval Research Laboratory

Evaluation of Delay Queues for a Ravenscar Hardware Kernel
Gustaf Naeser and Johan Furunas, Mälardalens University

Requirements Modeling within Iterative, Incremental Processes
Lars Pareto, Chalmers University

Estimation of Execution Times of On-Chip Multi-Processor Stream …
P. Poplavko, T. Basten, M. Pastrnak, J. van Meerbergen, Eindhoven University of Technology, M. Bekooij, Philips Research Laboratory, and P. de With, Eindhoven University of Technology

An Environment for Design Verification of Smart Card Systems Using Attack Simulation in SystemC
Klaus Rothbart, Ulrich Neffe, Christian Steger, and Reinhold Weiss, Graz University of Technology; Edgar Rieger and Andreas Muehlberger, Philips Semiconductors

A Race-free Hardware Modeling Language
Patrick Schaumont, University of California, Los Angeles, Sandeep Shukla, Virginia Tech, and Ingrid Verbauwhede, University of California, Los Angeles

Polynomial Model-Based Evaluation of the Branch Coverage Metric for Functional Verification of Hardware Systems
Iñigo Ugarte and Pablo Sanchez, University of Cantabria

Transition Traversal Coverage Estimation for Symbolic Model Checking
Xingwen Xu, Shinji Kimura, Waseda University, Kazunari Horikawa, Takehiko Tsuchiya, Toshiba University

18:00 - 20:00

• Conference Reception
  Welcoming cocktail at Polo Zanotto (University of Verona)

Wednesday, July 13

09:00 - 10:00

• Keynote Talk II

Chair: Robert de Simone, INRIA

Title: System Design Extreme Makeover
Daniel Gajski, University of California, Irvine

10:00 - 11:00

• Session 3: Software Verification

Chair: Elizabeth Leonard, Naval Research Laboratory

Verification of Parameterized Hierarchical State Machines Using Action Language Verifier
Tuba Yavuz-Kahveci and Tevfik Bultan, University of California, Santa Barbara

Verification of Low-level Crypto-Protocol Implementations Using Automated Theorem Proving
Jan JŸrjens, Technical University - München

11:00 - 11:30

• Coffee Break

11:30 - 13:30

• Session 4: System-Level Verification

Chair: Klaus Schneider, University of Kaiserslautern

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
Daniel Kroening, ETH Zürich, Natasha Sharygina, Software Engineering Institute

Translation-Based Co-Verification
Fei Xie, Xiaoyu Song, Haera Chung, Ranajoy Nandi, Portland State University

Synchronization Verification in System-Level Design with ILP Solvers
Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita, University of Tokyo

Improving SystemC simulation through Petri net reductions
Nick Savoiu, University of California, Irvine, Sandeep Shukla, Virginia Tech, and Rajesh Gupta, University of California, San Diego


13:30 - 15:00

• Lunch

15:00 - 16:00

• Panel 1: Software and Systems Engineering in the Automotive Industry

Chair: Manfred Broy, Technical University – München
Panelists: Ingolf Kruger, University of California, San Diego, Wolfgang Pree, University of Constance

16:00 - 16:30

• Coffee Break

16:30 - 17:30

• Panel 1: Software and Systems Engineering in the Automotive Industry (cont.)

20:00 - 23:30

• Social dinner in Valpolicella

Thursday, July 14

09:00 - 10:00

• Keynote Talk III

Chair: Jean-Pierre Talpin, INRIA

Title: A Formal Approach to System-Level Design: Metamodels and Unified Design Environment
Keynote Speaker: Alberto Sangiovanni-Vincentelli, University of California, Berkeley

10:00 - 11:00

• Session 5: Model Checking

Chair: Daniel Kroening, ETH Zürich

Refinement Verification of Fair Transition Systems Can Contribute to PLTL Model Checking
FrançoiseFrançoise Bellegarde, Université de Franche-Compté, Samir Chouali, LORIA UMR, and Jacques Julliand, Université de Franche-Compté

Three-Valued Logic in Bounded Model Checking
Tobias Schuele, Klaus Schneider, University of Kaiserslautern

11:00 - 11:30

• Coffee Break

11:30 - 12:30

• Session 6: Micro-Architectural Specification and Verification

Chair: John O’Leary, Intel

A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines
Panagiotis Manolios, Sudarshan K. Srinivasan, Georgia Institute of Technology

On the question of decidability of shared memory consistency verification
Ali Sezgin, Ganesh Gopalakrishnan, University of Utah

12:30 - 13:30

• Session 7: Core Algorithms

Chair: Franco Fummi, University of Verona

Thunderstriking Constraints with Jupiter
Christos Kloukinas, City University, London

On the use of a High-level fault model to analyze the Logical Consequences of Properties
Stefano Brait, Franco Fummi, Graziano Pravadelli, University of Verona

13:30 - 15:00

• Lunch

15:00 - 16:30

• Panel 2: Design for Verification

Chair: Tevfik Bultan, University of California, Santa Barbara
Panelists: Byron Cook, Microsoft, Robert Kurshan, Cadence, Constance Heitmeyer, Naval Research Laboratory, John O’Leary, Intel

16:30 - 17:00

• Conference Close

17:00 - 17:30

• Coffee Break

17:30

• Tour of Verona

21:00

• Performance of “Aida” by Giuseppe Verdi at the Arena di Verona (optional)

Friday, July 15

Globally Asynchronous Locally Synchronous Design (FMGALS’2005)

08:30 - 09:00

• Registration

09:00 - 10:00

• Keynote - Chair: Rajesh Gupta

Tag Systems: a Formal Model for Heterogeneous System Analysis and Designto
Alberto Sangiovanni Vicentelli, University of California at Berkeley Gupta

10:00 -10:30

• Coffee Break

10:30 - 12:00

• Session I - Chair: Sandeep Shukla

10:30
Design challenges for a differential power analysis ware GALS based AES crypto-ASIC
Frank Gurkaynak, Stephan Oetiker, Hubert Kaeslin, Norbert Felber, Wolgang Fichtner.

10:55
A verification approach for GALS integration of synchronous components.
Frederic Doucet, Massimiliano Menarini, Ingolf H. Kruger, Jean-Pierre Talpin, Rajesh Gupta.

11:20
Another glance at relay stations in latency-insensitive design.
Julien Boucaron, Jean-Vivien Millo, Robert de Simone.

11:45
A functional programming framework for latency insensitive protocol validation.
Syed Suhaib, Deepak Mathaikutty, Sandeep Shukla, David Berner, Jean-Pierre Talpin.

12:00 - 14:00

• Lunch

14:00 - 15:00

• Session II - Chair: Ken Stevens

14:00
The role of back-pressure in implementing latency-insensitive systems
Luca Carloni

14:25
Multi-Clock Latency-Insensitive Architecture and Wrapper Synthesis
Ankur Agiwal and Montek Singh

14:50
Opportunities and challenges in process-algebraic verification of asynchronous circuit designs
Xu Wang, Marta Kwiatkowska and G. Theodoropoulos

15:05 - 15:35

• Coffee Break

15:35 - 16:40

• Session III - Chair: Jean-Pierre Talpin

15:35
GALS Test Chip on 130nm Process.
David Bormann.

16:00
From weakly endochronous systems to delay-insensitive circuits.
Sohini Dasgupta, Dumitru Potop-Butucaru, Benoit Caillaud, Alexandre Yakovlev.

16:25
A survey of desynchronization in a polychronous model of computation.
Julien Ouy.

16:40 - 18:00

• Panel - Chair: Montek Singh

18:00

• End of the workshop

Réalisation Axome - Création de sites Internet