1. FMCAD 1996: Palo Alto, California, USA

@proceedings{DBLP:conf/fmcad/1996,
  editor    = {Mandayam K. Srivas and
               Albert John Camilleri},
  title     = {Formal Methods in Computer-Aided Design, First International
               Conference, FMCAD '96, Palo Alto, California, USA, November 6-8,
               1996, Proceedings},
  booktitle = {FMCAD},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1166},
  year      = {1996},
  isbn      = {3-540-61937-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

• Kurt Keutzer: The Need for Formal Methods for Integrated Circuit Design. 1-18
• Yirng-An Chen, Edmund M. Clarke, Pei-Hsin Ho, Yatin Vasant Hoskote, Timothy Kam, Manpreet Khaira, John W. O'Leary, Xudong Zhao: Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. 19-33
• Laurent Arditi: BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions. 34-48
• Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi: Modular Verification of Multipliers. 49-63
• Paul S. Miner, James F. Leathrum: Verification of IEEE Compliant Subtractive Division Algorithms. 64-78
• Harald Rueß: Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study. 79-93
• Francisco J. Cantu, Alan Bundy, Alan Smaill, David A. Basin: Experiments in Automating Hardware Verification Using Inductive Proof Planning. 94-108
• Alok Jain, Kyle L. Nelson, Randal E. Bryant: Verifying Nondeterministic Implementations of Deterministic Systems. 109-125
• Daniel Lewin, Dean H. Lorenz, Shmuel Ur: A Methodology for Processor Implementation Verification. 126-142
• Daniel Geist, Monica Farkas, Avner Landver, Yossi Lichtenstein, Shmuel Ur, Yaron Wolfsthal: Coverage-Directed Test Generation Using Symbolic Techniques. 143-158
• Robert B. Jones, Carl-Johan H. Seger, David L. Dill: Self-Consistency Checking. 159-171
• David Cyrluk: Inverting the Abstraction Mapping: A Methodology for Hardware Verification. 172-186
• Clark W. Barrett, David L. Dill, Jeremy R. Levitt: Validity Checking for Combinations of Theories with Equality. 187-201
• Klaus Schneider, Thomas Kropf: A Unified Approach for Combining Different Formalisms for Hardware Verification. 202-217
• Ramin Hojati, Adrian J. Isles, Desmond Kirkpatrick, Robert K. Brayton: Verification Using Uninterpreted Functions and Finite Instantiations. 218-232
• Zijian Zhou, Xiaoyu Song, Sofiène Tahar, Eduard Cerny, Francisco Corella, Michel Langevin: Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs. 233-247
• Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa: VIS. 248-256
• Natarajan Shankar: PVS: Combining Specification, Proof Checking, and Model Checking. 257-264
• John Harrison: HOL Light: A Tutorial Introduction. 265-269
• Bhaskar Bose, M. Esen Tuna, Venkatesh Choppella: A Tutorial on Digital Design Derivation Using DRS. 270-274
• Bishop Brock, Matt Kaufmann, J. Strother Moore: ACL2 Theorems About Commercial Microprocessors. 275-293
• Ramayya Kumar, Christian Blumenröhr, Dirk Eisenbiegler, Detlef Schmid: Formal Synthesis in Circuit Design - A Classification and Survey. 294-309
• Mark Bickford, Damir Jamsek: Formal Specification and Verification of VHDL. 310-326
• Naren Narasimhan, Ranga Vemuri: Specification of Control Flow Properties for Verification of Synthesized VHDL Designs. 327-345
• Anthony C. J. Fox, Neal A. Harman: An Algebraic Model of Correctness for Superscalar Microprocessors. 346-361
• Phillip J. Windley, Jerry R. Burch: Mechanically Checking a Lemma Used in an Automatic Verification Tool. 362-376
• Jeffrey X. Su, David L. Dill, Clark W. Barrett: Automatic Generation of Invariants in Processor Verification. 377-388
• Ellen Sentovich: A Brief Study of BDD Package Performance. 389-403
• Christoph Meinel, Thorsten Theobald: Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines. 404-418
• Jawahar Jain, Amit Narayan, C. Coelho, Sunil P. Khatri, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton, Masahiro Fujita: Decomposition Techniques for Efficient ROBDD Construction. 419-434
• Tomohiro Yoneda, Hideyuki Hatori, Atsushi Takahara, Shin-ichi Minato: BDDs vs. Zero-Suppressed BDDs: for CTL Symbolic Model Checking of Petri Nets. 435-449
• Dominique Borrione, H. Bouamama, David Déharbe, C. Le Faou, Ayman M. Wahba: HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment. 450-467