AMAST Mail 1996
[Prev][Next][Index]

FMCAD'96: Preliminary Program Announcement (With apologies for duplicated receival)


                   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. 1) 			Late (after Sept. 1
_____ 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:____________________________________________________________

==================================================================================

PRELIMINARY PROGRAM
--------------------

(I) BDDs and Enhancements
--------------------------
A Study of the Performance of BDD Packages,
Ellen M. Sentowich (Ecole des Mines de Paris, France)

Local Encoding Transformations for Optimizing OBDD-Representations
of Finite State Machines,
Christoph Meinel and Thorsten Theobald (University of Trier, Germany)

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)

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)

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)

(II) Microprocessor Verification Techniques
-------------------------------------------
An Algebraic Model of Correctness for Superscalar Microprocessors,
A.C.J. Fox and N.A. Harman (University of Wales Swansea, UK)

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)

Automatic Generation of Invariants in Processor Verification,
Jeffrey X. Su, David L. Dill, and Clark Barrett (Stanford U, USA)

Inverting the Abstraction Mapping: A Methodology for Hardware
Verification,
David Cyrluk (Stanford U and SRI International, USA)


(III) Arithmetic Circuit Verification
--------------------------------------
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)

Verification of IEEE Compliant Subtractive Division Algorithms,
Paul S. Miner (NASA, Langley, USA) and James F. Leathrum, Jr. (Old
Dominion U., USA)

Hierarchical Verification of Two-Dimensional High-Speed
Multiplication in PVS: A Case Study,} Harald Ruess (U. Ulm, Germany)

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)

Modular Verification of Multipliers,
K. Ravi, A. Pardo, G.D. Hachtel, and F. Somenzi (U Colorado, USA)


(IV) Combined Approaches to Hardware Verification
-------------------------------------------------
A Unified Approach for Combining Different Formalisms for Hardware
Verification,}
Klaus Schneider and Thomas Kropf (U Karlsruhe, Germany)

Verification Using Uninterpreted Functions and Finite Instantiations,
Ramin Hojati, Adrian Isles, Desmond Kirkpatrick, and Robert K. Brayton
(UC Berkeley, USA)

BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic
Assembly Instructions,
Laurent Arditi (CNRS, France)

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)


(V) Formal Methods for Synthesis and VHDL
-----------------------------------------
Formal Specification and Verification of VHDL,
Mark Bickford and Damir Jamsek (ORA Corporation, USA)

Specification of Control Flow Properties for Verification of
Synthesized VHDL Designs,
Naren Narasimhan and Ranga Vemuri (U Cincinnati, USA)

Formal Synthesis in Circuit Design - A Survey,
R. Kumar (Forschungzentrum Informatik, Karlsruhe, Germany), C. Blumenrohr,
D. Eisenbiegler, and D. Schmid (U Karlsruhe, Germany)

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)

(VI) Pragmatic Approaches to Verification
-------------------------------------------
Self-Consistency Checking,
Robert B. Jones, Carl-Johan H. Seger (Intel Corp., USA), and David L. Dill
(Stanford U, USA)

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)

A Methodology for Processor Implementation Verification,
Daniel M. Lewin, Dean H. Lorenz (Israel Inst. of Technology), and Shmuel
Ur (IBM Science and Technology, Israel)
[ AMAST Mail 1996 | Latest Update | AMAST Mail Meta-Index | AMAST ]