1. FMCAD 1996:
Palo Alto, California, USA
Mandayam K. Srivas, Albert John Camilleri (Eds.):
Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings.
Lecture Notes in Computer Science 1166 Springer 1996, ISBN 3-540-61937-2 BibTeX
@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 BibTeX
- 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 BibTeX
- Laurent Arditi:
BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions.
34-48 BibTeX
- Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi:
Modular Verification of Multipliers.
49-63 BibTeX
- Paul S. Miner, James F. Leathrum:
Verification of IEEE Compliant Subtractive Division Algorithms.
64-78 BibTeX
- Harald Rueß:
Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study.
79-93 BibTeX
- Francisco J. Cantu, Alan Bundy, Alan Smaill, David A. Basin:
Experiments in Automating Hardware Verification Using Inductive Proof Planning.
94-108 BibTeX
- Alok Jain, Kyle L. Nelson, Randal E. Bryant:
Verifying Nondeterministic Implementations of Deterministic Systems.
109-125 BibTeX
- Daniel Lewin, Dean H. Lorenz, Shmuel Ur:
A Methodology for Processor Implementation Verification.
126-142 BibTeX
- Daniel Geist, Monica Farkas, Avner Landver, Yossi Lichtenstein, Shmuel Ur, Yaron Wolfsthal:
Coverage-Directed Test Generation Using Symbolic Techniques.
143-158 BibTeX
- Robert B. Jones, Carl-Johan H. Seger, David L. Dill:
Self-Consistency Checking.
159-171 BibTeX
- David Cyrluk:
Inverting the Abstraction Mapping: A Methodology for Hardware Verification.
172-186 BibTeX
- Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
Validity Checking for Combinations of Theories with Equality.
187-201 BibTeX
- Klaus Schneider, Thomas Kropf:
A Unified Approach for Combining Different Formalisms for Hardware Verification.
202-217 BibTeX
- Ramin Hojati, Adrian J. Isles, Desmond Kirkpatrick, Robert K. Brayton:
Verification Using Uninterpreted Functions and Finite Instantiations.
218-232 BibTeX
- 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 BibTeX
- 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 BibTeX
- Natarajan Shankar:
PVS: Combining Specification, Proof Checking, and Model Checking.
257-264 BibTeX
- John Harrison:
HOL Light: A Tutorial Introduction.
265-269 BibTeX
- Bhaskar Bose, M. Esen Tuna, Venkatesh Choppella:
A Tutorial on Digital Design Derivation Using DRS.
270-274 BibTeX
- Bishop Brock, Matt Kaufmann, J. Strother Moore:
ACL2 Theorems About Commercial Microprocessors.
275-293 BibTeX
- Ramayya Kumar, Christian Blumenröhr, Dirk Eisenbiegler, Detlef Schmid:
Formal Synthesis in Circuit Design - A Classification and Survey.
294-309 BibTeX
- Mark Bickford, Damir Jamsek:
Formal Specification and Verification of VHDL.
310-326 BibTeX
- Naren Narasimhan, Ranga Vemuri:
Specification of Control Flow Properties for Verification of Synthesized VHDL Designs.
327-345 BibTeX
- Anthony C. J. Fox, Neal A. Harman:
An Algebraic Model of Correctness for Superscalar Microprocessors.
346-361 BibTeX
- Phillip J. Windley, Jerry R. Burch:
Mechanically Checking a Lemma Used in an Automatic Verification Tool.
362-376 BibTeX
- Jeffrey X. Su, David L. Dill, Clark W. Barrett:
Automatic Generation of Invariants in Processor Verification.
377-388 BibTeX
- Ellen Sentovich:
A Brief Study of BDD Package Performance.
389-403 BibTeX
- Christoph Meinel, Thorsten Theobald:
Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines.
404-418 BibTeX
- 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 BibTeX
- Tomohiro Yoneda, Hideyuki Hatori, Atsushi Takahara, Shin-ichi Minato:
BDDs vs. Zero-Suppressed BDDs: for CTL Symbolic Model Checking of Petri Nets.
435-449 BibTeX
- 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 BibTeX
Copyright © Sat May 16 23:12:16 2009
by Michael Ley (ley@uni-trier.de)