- Authors:
- E. M. Clarke
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA
,School of Computer Science, Carnegie Mellon University, Pittsburgh, PA
View Profile - M. Khaira
Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
,Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
View Profile - X. Zhao
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
View Profile - Authors Info & Affiliations
- 21citation
- 321 Downloads
- Get Citation Alerts
This alert has been successfully added and will be sent to:
You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below.
Manage my AlertsPleaselog in to your account
- Save to Binder
- Export Citation
- Publisher Site
DAC '96: Proceedings of the 33rd annual Design Automation Conference
Word level model checking—avoiding the Pentium FDIV error

References
- 1.R. E. Bryant and Y. A. Chen. Verification of arithmetic functions with Binary Moment Diagrams. In Proceedings of the 31tnd A CM/IEEE Design Automation Con- }erence, pages 535-541. IEEE Computer Society Press, June 1995.Google Scholar
Digital Library
- 2.J. R. Butch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model check, g: 102o states and beyond. Information and Computation, 98(2):142- 170, June 1992.Google Scholar
Digital Library
- 3.E. M. Clarke and E. A. Emerson. synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Vedag, 1981.Google Scholar
Digital Library
- 4.E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.Google Scholar
Digital Library
- 5.E. M. Clarke, M. Fujita, and X. Zhao. Hybrid Decision Diagrams- overcoming the limitations of MTBDDs and BMDs. In Proceedings o} the 1995Proceedings o/ the IEEE International Conference on Computer Aided Design, pages 159-183. IEEE Computer Society Press, November 1995.Google Scholar
Digital Library
- 6.E. M. Clarke and X. Zhao. Analytica: A theorem prover for Mathematica. The Journal of Mathematica, 3(1), 1993.Google Scholar
- 7.K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
Digital Library
- 8.G. S. Taylor. Compatible hardware for division and square root. In Proceedings of the Fifth IEEE Symposium on Computer Arithmetic, 1993.Google Scholar
Index Terms
Word level model checking—avoiding the Pentium FDIV error
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
Published in
DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996839 pagesISBN:0897917790DOI:10.1145/240518- Chairmans:
- Thomas P. Pennino
Bell Labs, Holmdel, NJ
, - Ellen J. Yoffa
IBM Corp., Yorktown Heights, NY
Copyright © 1996 ACM
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
- Published: 1 June 1996
Permissions
Request permissions about this article.
Request PermissionsQualifiers
- Article
Conference
Acceptance Rates
DAC '96 Paper Acceptance Rate 142of 377submissions, 38%
Overall Acceptance Rate 3,150of 10,963submissions, 29%
Upcoming Conference
Funding Sources
Article Metrics
- View Citations21Total Citations
- 321Total Downloads
- Downloads (Last 12 months)36
- Downloads (Last 6 weeks)6
Other Metrics
PDF Format
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderDigital Edition
View this article in digital edition.
View Digital Edition