Second ACM/IEEE International Conference on

Formal Methods and Models for Co-Design


June 23-25, 2004

San Diego Hilton, San Diego, California, USA

Preliminary Program

DAY 1:  Wednesday, June 23, 2004

0845  Program Chairs Welcome: Connie Heitmeyer, NRL, and Jean-Pierre Talpin, INRIA Rennes

0900  Keynote Talk I -- Chair: Rajesh Gupta, UC -- San Diego

System Modeling and Verification with UCLID

Randy Bryant, Carnegie Mellon U.

1000  --------------------------------------------------Break--------------------------------------------------

1030  Session I:  Model Checking -- Chair: Jens Palsberg, UC -- Los Angeles

Verification of SpecC and Verilog Using Predicate Abstraction

Daniel Kroening, Edmund Clarke, and Himanshu Jain, Carnegie Mellon U.

Model Checking of Infinite State Systems: Exploiting the Automata Hierarchy

Tobias Schuele and Klaus Schneider, U. of Kaiserslautern

Check and Simulate: A Case for Incorporating Model Checking in Network Simulation

Ahmed Sobeih, Jennifer C. Hou, and Mahesh Viswanathan, U. Illinois at Urbana-Champaign

1200  --------------------------------------------------Lunch-------------------------------------------------

1330  Session II:  Modeling Languages -- Chair: R. K. Shyamasundar, TIFR.

Curing Schizophrenia by Program Rewriting in Esterel

Olivier Tardieu and Robert de Simone, INRIA Sophia Antopolis

Synchronous Extensions to Operation-Centric Hardware Description Languages

Grace Nordin and James C. Hoe, Carnegie Mellon U.

PROBMELA: A Modeling Language for Communicating Probabilistic Processes

Christel Baier, Frank Ciesinski, and Marcus Groesser, U. Bonn

1500  --------------------------------------------------Break--------------------------------------------------

1530  Tutorial -- Chair: Arvind, MIT

Bluespec SystemVerilog: Efficient, Correct RTL from High-level Specifications

Rishiyur Nikhil, CTO, Bluespec Inc.
1630  Session III:  Synthesis -- Chair
: Jean-Pierre Talpin, INRIA Rennes

Using Invariants to Optimize Formal Specifications in Support of Efficient Code Synthesis

Ralph D. Jeffords and Elizabeth I. Leonard, Naval Research Laboratory

Efficient Code Synthesis from Synchronous Dataflow Graphs

Dag Bjorklund, Turku Centre for Computer Science

Designing a Reorder Buffer in Bluespec

Nirav Dave, MIT

1800  ----------------------------------------End of DAY 1-------------------------------------------------

1900  Welcome Reception

DAY 2:  Thursday, June 24, 2004

0900  Keynote Talk II  -- Chair : Constance Heitmeyer

The battle of accountable voting systems

David Dill, Stanford University

1000  --------------------------------------------------Break--------------------------------------------------

1030  Session IV: -- Formal Verification -- Chair: Carl Pixley, Synopsis

Static Priority Scheduling of Event-Triggered Real-Time Embedded Systems.

Cagkan Erbas and Andy Pimentel, U. of Amsterdam, Selin Erbas, U. Catholique de Louvain

The BUSpec Platform for Generation of Verification Aids for Standard Bus Protocols

Bhaskar Pal, Ansuman Banerjee, Pallab Dasgupta, and P. Chakrabarti, Indian Institute of Technology

Formal Verification of Pipelined Processors with Precise Exceptions

K. Kalyanasundaram and R. K. Shyamasundar, Tata Institute of Fundamental Research

1200  -------------------------------------------------Lunch-------------------------------------------------

1330  Industry Panel -- Chair: Tevfik Bultan, UC Santa Barbara

Discussion Topic:  Given that hardware verification has been such an uphill battle, what is the future of software verification?


Brian Bailey, Mentor Graphics                                  "The hurdles for acceptance of formal technologies"

Gerard Holzman, Jet Propulsion Laboratory          "Formal methods and software reliability" 

Bob Kurshan, Cadence                                             "Formal Verification As a Technology Transfer Problem"

Vladimir Levin, Microsoft                                           "Static Driver Verifier, a formal verification tool aimed at Windows
device drivers"

John O'Leary, Intel                                                     "Formal Verification in Intel CPU Design"

Carl Pixley, Synopsis                                                "Designers Want Proofs! But Show Me the Money"

1530  --------------------------------------------------Break--------------------------------------------------

1600  Industry Panel Discussion -- Chair : Sandeep Shukla, Virginia Tech

1730  Wine and Cheese Party

Poster Session -- Chair : Arvind, MIT

Work in Progress

2000  ---------------------------------------------End of DAY 2---------------------------------------------

DAY 3 :  Friday, June 25, 2004

0900  Keynote Talk III  -- Chair: Arvind, MIT

Actor-Oriented Design

Edward Lee, UC - Berkeley

1000  --------------------------------------------------Break--------------------------------------------------

1030  Session V:  Simulation and Testing -- Chair: Harry Foster, Jasper

Checkers for SystemC Designs

Daniel Grosse and Rolf Drechsler, U. Bremen

Hierarchical Reconfiguration of Dataflow Models

Stephen Neuendorffer and Edward Lee, UC - Berkeley

The Ephemeral History Register: Flexible Scheduling for Rule-Based Designs

Daniel L. Rosenband, MIT

1200  -------------------------------------------------Lunch-------------------------------------------------

1315  Session VI:  Compositional Verification -- Chair: Franco Fummi, U. di Verona

Automated, Compositional and Iterative Deadlock Detection

Sagar Chaki, Edmund Clarke, Joel Ouaknine, and Natasha Sharygina, Carnegie Mellon U.

Compositional Verification for Secure Loading of Smart Card Applets

Christoph Sprenger, Ch. Du Couchant, and Dilian Gurov, Royal Institute of Technology, and Marieke Huisman, INRIA Sophia Antipolis

A Framework for Heterogeneous Formal Modelling and Compositional Verification of Avionics Systems

Yamine Ait-Ameur, U. de Poitiers, Remi Delmas and Virginie Wiels, ONERA-CERT

1445  Program Chairs Closing Remarks: Connie Heitmeyer and Jean-Pierre Talpin

1500  ------------------------------------End of MEMOCODE 2004-------------------------------------

1515  Organizing Committee Meeting for MEMOCODE 2005