AMAST Mail 1996
[Prev][Next][Index]
FMCAD'96: Conference Program (Early-registration-deadline: Sept 15, 1996)
-
Subject: FMCAD'96: Conference Program (Early-registration-deadline: Sept 15, 1996)
-
From: srivas <srivas@csl.sri.com>
-
Date: Mon, 9 Sep 1996 14:15:29 -0700 (PDT)
** Sincere apologies for multiple receptions **
A Forum for State-of-the-art Tools and
Techniques
Based on Formal Methods for Computer-Aided
Design of Hardware
+---------------------------------------------------------------------+
| FMCAD '96 |
| |
| International Conference on Formal Methods in Computer-Aided Design |
| (Successor to Theorem Provers in Circuit Design) |
| |
| 6 -- 8 November |
| Holiday Inn, Palo Alto, California, USA |
| In the Heart of Silicon Valley |
+---------------------------------------------------------------------+
Sponsored by
SRI International * IFIP WG 10.5 *
Cadence Berkeley Labs * Hewlett-Packard Company
LSI Logic Corporation * Rockwell International
Synopsys, Inc. * Texas Instruments, Inc.
INTENDED PARTICIPANTS:
Researchers as well as practicing digital design engineers
interested in hardware verification, synthesis and testing.
INVITED SPEAKERS:
-----------------
o David Dill, Stanford University, USA
o Kurt Keutzer, Synopsys Inc., USA
o J S. Moore, Computational Logic Inc., USA
TUTORIALS
---------
VIS: A System for Verification and Synthesis,} R.K. Brayton, et al.
(UC Berkeley, USA)
PVS: Combining Specification, Proof Checking, and Model Checking,
N. Shankar et al. (SRI International, USA)
============================================================================
Conference Organizers
---------------------
General and Program Chair: M. K. Srivas, (SRI International, USA)
Tutorial Chair: A. Camilleri (Hewlett-Packard Company, USA)
PROGRAM COMMITTEE:
D. Borrione (TIMA, France)
R. Brayton (University of California, Berkeley, USA)
R. Bryant (CMU, USA)
R. Camposano (Synopsys Inc., USA)
L. Claesen (IMEC, Belgium)
E. Clarke (CMU, USA)
C. Delgado Kloos (Universidad Politecnica de Madrid, Spain)
M. Fujita (Fujitsu Labs, USA)
S. German (IBM, Yorktown Heights, USA)
M. Gordon (University of Cambridge, UK)
O. Grumberg (Technion, Haifa, Israel)
W. Hunt (Computational Logic, Inc., USA)
S. Johnson (University of Indiana, USA)
R. Kumar (FZI, Karlsruhe, Germany)
M. Leeser (Northeastern University, USA)
P. Loewenstein (Sun Microsystems, USA)
K. McMillan (Cadence Berkeley Lab, USA)
C. Seger (Intel, Oregon, USA)
J. Staunstrup (Technical University, Denmark)
V. Stavridou (Queen Mary and Westfield College, UK)
P.A. Subrahmanyam (AT&T, USA)
J. Van Tassel (Texas Instruments, USA)
================================================================================
General Information: http://www.csl.sri.com/FMCAD96; tel: +1 415/859-5924;
fax: +1 415/859-2844; email: burgess@csl.sri.com.
HOTEL INFORMATION
-----------------
Hotel: The conference will be held at the Holiday Inn, Palo Alto. A
special rate of $99.00 single or $109.00 double is available until October
22. Call +1 415/328-2800, fax: +415/327-7362 for
reservations, referring to FMCAD for the special rate.
REGISTRATION
------------
Send the form below with your check or bank draft payable to SRI International
- FMCAD96, in U.S. dollars, drawn on a U.S. Bank. We regret we cannot
accept any credit cards. If you cannot send a draft in U.S. dollars on a
U.S. Bank, please contact burgess@csl.sri.com.
Send to: Judith Burgess, SRI
International, 333 Ravenswood Ave., Menlo Park, CA 94025, USA.
=========================================================================
Early (before Sept. 15) Late (after Sept. 15)
_____ Regular $275 _____ Regular $375
_____ Student $150 _____ Student $150
Name________________________________________________________________________
Affiliation_________________________________________________________________
Address_____________________________________________________________________
____________________________________________________________________________
Phone_________________ fax__________________email___________________________
Dietary Restrictions: ___________________________________
If you are a full-time student, please include a photocopy of your student
I.D. card, give the name of your academic sponsor below.
Name of sponsor:____________________________________________________________
=============================================================================
CONFERENCE PROGRAM
=============================================================================
NOVEMBER 6, 1996 (Wednesday)
8:00 -- 8:50 Late Registration
9:00 -- 10:00 Invited Talk: Kurt Keutzer, Synopsys, Inc.
The Need for Formal Methods for Integrated Circuit Design
10:00 -- 10:15 BREAK
Session I: Verification Using Enhanced BDDs
-------------------------------------------
10:15 -- 10:45 Verification of a Complete Floating-Point Unit Using Word-Level
Model Checking,
P.-H. Ho, Y. Hoskote, T Kam, M. Khaira, J. O'Leary, X Zhao (Intel
Development Labs, USA), Y-A. Chen and E. Clarke (Carnegie Mellon U, USA)
10:45 -- 11:15 BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic
Assembly Instructions,
Laurent Arditi (CNRS, France)
11:15 -- 11:45 Modular Verification of Multipliers,
K. Ravi, A. Pardo, G.D. Hachtel, and F. Somenzi (U Colorado, USA)
11:45 -- 1:00 LUNCH
1:00 -- 2:30 Session II: Arithmetic Circuit Verification
------------------------------------------------------------
1:00 -- 1:30 Verification of IEEE Compliant Subtractive Division Algorithms,
Paul S. Miner (NASA, Langley, USA) and James F. Leathrum, Jr. (Old
Dominion U., USA)
1:30 -- 2:00 Hierarchical Verification of Two-Dimensional High-Speed
Multiplication in PVS: A Case Study,} Harald Ruess (U. Ulm, Germany)
2:00 -- 2:30 Automating Hardware Verification Using Inductive Proof Planning,
Francisco J. Cantu (Monterrey TU, Mexico), Alan Bundy, Alan Smaill (U
Edinburgh, UK), and David Basin (MPI, Germany)
2:30 -- 2:45 BREAK
Session III: Verification by Symbolic Simulation
------------------------------------------------
2:45 -- 3:15 Verifying Nondeterministic Implementations of Deterministic Systems
Alok Jain (Carnegie Mellon U, USA), Kyle Nelson (IBM Rochester, USA), and
Randal E. Bryant (Carnegie Mellon U, USA)
3:15 -- 3:45 A Methodology for Processor Implementation Verification,
Daniel M. Lewin, Dean H. Lorenz (Israel Inst. of Technology), and Shmuel
Ur (IBM Science and Technology, Israel)
3:45 -- 4:15 Coverage-directed Test Generation Using Symbolic Techniques,
Danny Geist, Monica Farkas, Avner Landver, Yossi Lichtenstein,
Shmuel Ur, and Yaron Wolfsthal (IBM Science and Technology, Israel)
4:15 -- 4:30 BREAK
Session IV: Verification Methodology
------------------------------------
4:30 -- 5: 00 Self-Consistency Checking,
Robert B. Jones, Carl-Johan H. Seger (Intel Corp., USA),
and David L. Dill (Stanford U, USA)
5:00 -- 5:30 Inverting the Abstraction Mapping: A Methodology for Hardware Verification,
David Cyrluk (Stanford U and SRI International, USA)
NOVEMBER 7, 1996 (Thursday)
9:00 -- 10:00 INVITED TALK: David Dill, Stanford University
Validity Checking for Combinations of Theories with Equality
10:00 -- 10:15 BREAK
Session V: Combined Approaches for Verification
-----------------------------------------------
10:15 -- 10:45 A Unified Approach for Combining Different Formalisms for
Hardware Verification,
Klaus Schneider and Thomas Kropf (U Karlsruhe, Germany)
10:45 -- 11:15 Verification Using Uninterpreted Functions and Finite Instantiations,
Ramin Hojati, Adrian Isles, Desmond Kirkpatrick, and Robert K. Brayton
(UC Berkeley, USA)
11:15 -- 11:45 Verification of the Island Tunnel Controller using Multiway
Decision Graphs,
Z. Zhou, X. Song, S. Tahar, E. Cerny (U Montreal, Canada), F. Corella
(Hewlett-Packard Co, USA), and M. Langevin (GMD-SET, Germany)
11:45 -- 1:00 LUNCH
1:00 -- 2:00 Tutorial I: R.K.Brayton, et al, University of California, Berkeley, USA
VIS
2:00 -- 2:15 BREAK
2:15 -- 3:15 Tutorial II: N. Shankar, SRI International, USA
PVS: Combining Specification, Proof Checking, and Model Checking
3:15 -- 3:30 BREAK
3:30 -- 4:15 Tutorial III: John Harrison, Abo Akademi University, Finland
HOL Light: A Tutorial Introduction
4:15 -- 5:00 Tutorial IV: B. Bose, M. E. Tuna, V. Choppella
A Tutorial on Digital Design Derivation Using DRS
6:30 Conference Dinner and Banquet
NOVEMBER 8, 1996 (Friday)
9:00 -- 10:00 INVITED TALK: J. S. Moore, Computational Logic, Inc., USA
ACL2 Theorems about Commercial Microprocessors
10:00 -- 10:15 BREAK
Session VI: Formal Methods for Synthesis and VHDL
-------------------------------------------------
10:15 -- 10:45 Formal Synthesis in Circuit Design - A Survey,
R. Kumar (Forschungzentrum Informatik, Karlsruhe, Germany),
C. Blumenrohr, D. Eisenbiegler, and D. Schmid (U Karlsruhe, Germany)
10:45 -- 11:15 Formal Specification and Verification of VHDL,
Mark Bickford and Damir Jamsek (ORA Corporation, USA)
11:15 -- 11:45 Specification of Control Flow Properties for Verification of
Synthesized VHDL Designs,
Naren Narasimhan and Ranga Vemuri (U Cincinnati, USA)
11:45 -- 1:00 LUNCH
Session VII: Microprocessor Verification Techniques
---------------------------------------------------
1:00 -- 1:30 An Algebraic Model of Correctness for Superscalar Microprocessors,
A.C.J. Fox and N.A. Harman (University of Wales Swansea, UK)
1:30 -- 2:00 Mechanically Checking a Lemma Used in an Automatic Verification Tool,
Phillip J. Windley (Brigham Young Univ, USA) and Jerry R. Burch (Cadence
Berkeley Labs, USA)
2:00 - 2:30 Automatic Generation of Invariants in Processor Verification,
Jeffrey X. Su, David L. Dill, and Clark Barrett (Stanford U, USA)
2:30 -- 2:45 BREAK
Session VIII: BDDs and Optimizations
-------------------------------------
2:45 -- 3: 15 A Study of the Performance of BDD Packages,
Ellen M. Sentowich (Ecole des Mines de Paris, France)
3:15 -- 3:45 Local Encoding Transformations for Optimizing OBDD-Representations
of Finite State Machines,
Christoph Meinel and Thorsten Theobald (University of Trier, Germany)
3:45 -- 4:15 Decomposition Techniques for Efficient ROBDD Construction,
Jawahar Jain (Fujitsu Labs, USA), Amit Narayan (UC Berkeley, USA),
Claudionor Coelho (Stanford U, USA), Sunil P. Khatri (UC Berkeley, USA),
A. Sangiovanni-Vincentelli (UC Berkeley, USA), R.K. Brayton (UC Berkeley,
USA), and M. Fujita (Fujitsu Labs, USA)
4:15 -- 4:30 BREAK
4:30 -- 5:30 Session IX: CAD Environment
-------------------------------------------
4:30 -- 5:00 BDDs vs. Zero-Suppressed BDDs : for CTL symbolic model checking of
Peri nets,
Tomohiro Yoneda , Hideyuki Hatori (Tokyo Inst. of Technology), Atsuchi
Takahara, and Shin-ichi Minato (NTT LSI, Japan)
5:00 -- 5:30 HDL-based integration of formal methods and CAD tools in the Prevail
environment,
D. Borrione, H. Bouamama,D. Deharbe, C. Le Faou, and A. Wahba
(TIMA, Grenoble, France)
[
AMAST Mail 1996
|
Latest Update |
AMAST Mail Meta-Index |
AMAST
]