{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:14:21Z","timestamp":1725484461083},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000297"},{"type":"electronic","value":"9783540361039"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36103-0_47","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T23:15:07Z","timestamp":1179270907000},"page":"459-470","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Enabling Hardware Verification through Design Changes"],"prefix":"10.1007","author":[{"given":"Amr T.","family":"Abdel-Hamid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Harrison","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,10]]},"reference":[{"key":"47_CR1","volume-title":"M.A.Sc. Thesis","author":"A.T. Abdel-Hamid","year":"2001","unstructured":"A.T. Abdel-Hamid. A Hierarchical Verification of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL. M.A.Sc. Thesis, Concordia University, Department of Electrical and Computer Engineering, Montreal, Canada, April 2001."},{"key":"47_CR2","unstructured":"H.T. Bui, B. Khalaf, and S. Tahar. Table-Driven Floating-Point Exponential Function. Proc. IEEE Canadian Conference on Electrical & Computer Engineering, May 1999, pp. 450\u2013455."},{"key":"47_CR3","unstructured":"V.A. Carreno. Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL system. NASA Technical Memorandum 110189, September 1995."},{"key":"47_CR4","doi-asserted-by":"crossref","unstructured":"F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design, vol. 10, February 1997, pp. 7\u201346.","DOI":"10.1023\/A:1008663530211"},{"key":"47_CR5","doi-asserted-by":"crossref","unstructured":"P. Curzon and I. Leslie. Improving Hardware Designs whilst Simplifying their Proof. In Designing Correct Circuits, Workshops in Computing, British Computer Society, 1996.","DOI":"10.14236\/ewic\/DCC1996.1"},{"key":"47_CR6","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: a Theorem ProvinEnvironment for Higher-order Logic. Cambridge University Press, 1993."},{"key":"47_CR7","volume-title":"Technical Report number 428","author":"J.R. Harrison","year":"1997","unstructured":"J.R. Harrison. Floating Point Verification in HOL Light: The Exponential Function. Technical Report number 428, University of Cambridge Computer Laboratory. UK, June 1997."},{"key":"47_CR8","unstructured":"J.R. Harrison. Theorem Proving with the Real Numbers. Technical Report number 408, University of Cambridge Computer Laboratory, December 1996."},{"key":"47_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics","author":"J.R. Harrison","year":"1997","unstructured":"J.R. Harrison. Verifying the Accuracy of Polynomial Approximations in HOL. In Theorem Proving in Higher Order Logics, LNCS 1275, Springer Verlag, 1997, pp. 137\u2013152."},{"issue":"2","key":"47_CR10","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C. Kern","year":"1999","unstructured":"C. Kern, and M. R. Greenstreat. Formal verification in Hardware Design: A Survey. ACM transactions on Design Automation of Electronic Systems, vol. 4, no. 2, April 1999, pp. 123\u2013193.","journal-title":"ACM transactions on Design Automation of Electronic Systems"},{"key":"47_CR11","unstructured":"P.S. Miner. Defining the IEEE-854 Floating-Point Standard in PVS. NASA Technical Memorandum 110167, June 1995."},{"issue":"2","key":"47_CR12","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/63522.214389","volume":"15","author":"P.T.P. Tang","year":"1989","unstructured":"P.T.P. Tang. Table-Driven Implementation of the Exponential Function in IEEE Floating-Point Arithmetic. ACM Transactions on Mathematical Software, vol. 15, no. 2, 1989, pp. 144\u2013157.","journal-title":"ACM Transactions on Mathematical Software"},{"key":"47_CR13","unstructured":"M. Hasan, S. Tahar, and P. Curzon. Impact of Design Changes on Verification Using MDGs. Proc. IEEE Canadian Conference on Electrical & Computer Engineering, Halifax, Nova Scotia, Canada, May 2000, pp. 173\u2013178."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36103-0_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,21]],"date-time":"2020-04-21T21:29:20Z","timestamp":1587504560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36103-0_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000297","9783540361039"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-36103-0_47","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"10 October 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}