{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:20Z","timestamp":1725512000203},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709510"},{"type":"electronic","value":"9783540709527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70952-7_1","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T08:40:01Z","timestamp":1182847201000},"page":"1-22","source":"Crossref","is-referenced-by-count":5,"title":["Challenges for Formal Verification in Industrial Setting"],"prefix":"10.1007","author":[{"given":"Anna","family":"Slobodov\u00e1","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1145\/309847.309968","volume-title":"Proc. of the 36th ACM\/IEEE conference on Design Automation","author":"M. Aagaard","year":"1999","unstructured":"Aagaard, M., Jones, R., Seger, K.-J.: Formal Verification Using Parametric Representations of Boolean Constraints. In: Proc. of the 36th ACM\/IEEE conference on Design Automation, pp. 402\u2013407. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"1_CR2","first-page":"201","volume-title":"ACM\/IEEE Proc. of Design Automation Conference","author":"M. Aagaard","year":"2000","unstructured":"Aagaard, M., Jones, R., Kaivola, R.: Formal Verification of Iterative Algorithms in Microprocessors. In: ACM\/IEEE Proc. of Design Automation Conference, pp. 201\u2013206. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"1_CR3","first-page":"7","volume-title":"ACM\/IEEE Proc. of the International Conference on Computer-Aided Design","author":"M. Aagaard","year":"1995","unstructured":"Aagaard, M., Seger, K.-J.: The Formal Verification of a Pipelined Double-Precision IEEE Floating-Point Multiplier. In: ACM\/IEEE Proc. of the International Conference on Computer-Aided Design, pp. 7\u201310. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR5","unstructured":"Coe, T.: Inside the Pentium FDIV bug. Dr. Dobbs Journal, 129-135 (April 1996)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/BFb0028769","volume-title":"Computer Aided Verification","author":"Y.-A. Chen","year":"1998","unstructured":"Chen, Y.-A., Bryant, R.: Verification of Floating-Point Adders. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 488\u2013499. Springer, Heidelberg (1998)"},{"key":"1_CR7","unstructured":"Fisher, L.M.: Flaw reported in a new Intel chip. New York Times, May 6, D 4:3 (1997)"},{"key":"1_CR8","unstructured":"Flatau, A., Kaufmann, M., Russinoff, D., Smith, E., Sumners, R.: Formal Verification of Microprocessors at AMD. In: Designing Correct Circuits (2002)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_14","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal Verification of Floating-point Trigonometric Functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 217\u2013233. Springer, Heidelberg (2000)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-44659-1_15","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal Verification of IA-64 Division Algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 234\u2013251. Springer, Heidelberg (2000)"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J. Harrison","year":"2003","unstructured":"Harrison, J.: Formal Verification of Square Root Algorithms. Formal Methods in System Design\u00a022, 143\u2013153 (2003)","journal-title":"Formal Methods in System Design"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/11526841_35","volume-title":"FM 2005: Formal Methods","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: Floating-Point Verification. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 529\u2013532. Springer, Heidelberg (2005)"},{"key":"1_CR13","unstructured":"Formal Verification of a Fully IEEE Compliant Floating Point Unit. Dissertation, University of Saarbruecken (April 2002)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Jacobi, C., Weber, K., Paruthi, V., Baumgartner, J.: Automatic Formal Verification on Fused-Multiply-Add FPUs. In: Proc. of the conference on Design, automation and test in Europe (DATE) (2005)","DOI":"10.1109\/DATE.2005.75"},{"key":"1_CR15","volume-title":"Computer Arithmetic Algorithms","author":"I. Koren","year":"2002","unstructured":"Koren, I.: Computer Arithmetic Algorithms, 2nd edn. A.K.Peters, Wellesley (2002)","edition":"2"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-44659-1_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Kaivola","year":"2000","unstructured":"Kaivola, R., Aagard, M.: Divider Circuit Verification with Model Checking and Theorem Proving. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 338\u2013355. Springer, Heidelberg (2000)"},{"issue":"Issue 3","key":"1_CR17","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10009-002-0081-6","volume":"4","author":"R. Kaivola","year":"2003","unstructured":"Kaivola, R., Kohatsu, K.: Proof Engineering in the Large: Formal Verification of Pentium(R) Floating-Point Divider. Software Tools for Technology Transfer\u00a04(Issue 3), 323\u2013335 (2003)","journal-title":"Software Tools for Technology Transfer"},{"key":"1_CR18","unstructured":"Kaivola, R., Narasimhan, N.: Formal Verification of the Pentium(R) Floating-Point Multiplier. In: Proc. of the conference on Design, automation and test in Europe (DATE) (2002)"},{"issue":"Issue 1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/641876.641878","volume":"29","author":"Y. Nievergelt","year":"2003","unstructured":"Nievergelt, Y.: Scalar Fused Multiply-Add Instructions Produce Floating-Point Matrix Arithmetic Provably Accurate to the Penultimate Digit. ACM Transactions on Mathematical Software (TOMS)\u00a029(Issue 1), 27\u201348 (2003)","journal-title":"ACM Transactions on Mathematical Software (TOMS)"},{"key":"1_CR20","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.: Formally Verifying IEEE Compliance of Floating-point Hardware. Intel Technology Journal, Q1 1999 (1999)"},{"key":"1_CR21","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"D. Russinoff","year":"2000","unstructured":"Russinoff, D., Flatau, A.: Mechanical Verification of Register-Transfer Logic: A Floating-Point Multiplier. In: Kaufmann, M., Manolios, P., Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"1_CR22","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Russinoff","year":"1998","unstructured":"Russinoff, D.: A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD-K7 Floating-Point Multiplication, Division, and Square Root Instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998)","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-40922-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Russinoff","year":"2000","unstructured":"Russinoff, D.: A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon(TM) Processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 3\u201336. Springer, Heidelberg (2000)"},{"key":"1_CR24","first-page":"1","volume-title":"ACM\/IEEE Proc. of Design Automation Conference","author":"T. Schubert","year":"2003","unstructured":"Schubert, T.: High Level Formal Verification on Next-Generation Microprocessors. In: ACM\/IEEE Proc. of Design Automation Conference, pp. 1\u20136. IEEE Computer Society Press, Los Alamitos (2003)"},{"issue":"2","key":"1_CR25","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Design\u00a06(2), 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"1_CR26","unstructured":"Slobodov\u00e1, A., Nagalla, K.: Formal Verification of Floating-Point Multiply-Add on Itanium(R) Processor. In: Designing Correct Circuits (Unpublished Proc.), Barcelona, March (2004)"},{"key":"1_CR27","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"L. Paulson","year":"1996","unstructured":"Paulson, L.: ML for the Working Programmer. Cambridge University Press, Cambridge (1996)"},{"key":"1_CR28","unstructured":"IEEE Standard for Binary Floating-Point Arithmetic. ANSI\/IEEE Std 754-1985"},{"key":"1_CR29","unstructured":"Intel(R) Itanium(R) Architecture Software Developer\u2019s Manual. Revision 2.1, Document numbers: (245317-245319)-004, Intel Corporation (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Applications and Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70952-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T08:52:30Z","timestamp":1550393550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70952-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540709510","9783540709527"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70952-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}