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