Monday, July 11


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



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



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



15:00 - 16:30

Panel 2: Design for Verification

Chair:  Tevfik Bultan, University of California, Santa Barbara
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



Tour of Verona



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


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

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

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

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

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

12:00 - 14:00

14:00 - 15:00
Session II - Chair: Ken Stevens

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

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

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

GALS Test Chip on 130nm Process.
David Bormann.

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

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

16:40 - 18:00
Panel - Chair: Montek Singh

End of the workshop