Second
ACM/IEEE International Conference on
Formal
Methods and Models for Co-Design
MEMOCODE
2004
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?
Panelists:
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