{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,16]],"date-time":"2025-04-16T05:36:17Z","timestamp":1744781777311,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_4","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"37-51","source":"Crossref","is-referenced-by-count":8,"title":["A Methodology for the Formal Verification of FFT Algorithms in HOL"],"prefix":"10.1007","author":[{"given":"Behzad","family":"Akbarpour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-47884-1_11","volume-title":"Integrated Formal Methods","author":"B. Akbarpour","year":"2002","unstructured":"Akbarpour, B., Tahar, S., Dekdouk, A.: Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 185\u2013204. Springer, Heidelberg (2002)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-39893-6_13","volume-title":"Formal Methods and Software Engineering","author":"B. Akbarpour","year":"2003","unstructured":"Akbarpour, B., Tahar, S.: Modeling SystemC Fixed-Point Arithmetic in HOL. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 206\u2013225. Springer, Heidelberg (2003)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30142-4_1","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Akbarpour","year":"2004","unstructured":"Akbarpour, B., Tahar, S.: Error Analysis of Digital Filters using Theorem Proving. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 1\u201316. Springer, Heidelberg (2004)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-48683-6_33","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"1999","unstructured":"Bjesse, P.: Automatic Verification of Combinational and Pipelined FFT Circuits. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 380\u2013393. Springer, Heidelberg (1999)"},{"key":"4_CR5","first-page":"129","volume-title":"Theorem Provers in Circuit Design","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van-Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Theorem Provers in Circuit Design, pp. 129\u2013156. North-Holland, Amsterdam (1992)"},{"key":"4_CR6","volume-title":"The Fast Fourier Transform","author":"E.O. Brigham","year":"1974","unstructured":"Brigham, E.O.: The Fast Fourier Transform. Prentice Hall, Englewood Cliffs (1974)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-44755-5_12","volume-title":"Theorem Proving in Higher Order Logics","author":"V. Capretta","year":"2001","unstructured":"Capretta, V.: Certifying the Fast Fourier Transform with Coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 154\u2013168. Springer, Heidelberg (2001)"},{"key":"4_CR8","unstructured":"Synopsys, Inc. CoCentric TM System Studio User\u2019s Guide, USA (August 2001)"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/TAU.1967.1161899","volume":"AU-15","author":"W.T. Cochran","year":"1967","unstructured":"Cochran, W.T., et al.: What is the Fast Fourier Transform. IEEE Transactions on Audio and Electroacoustics\u00a0AU-15, 45\u201355 (1967)","journal-title":"IEEE Transactions on Audio and Electroacoustics"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1090\/S0025-5718-1965-0178586-1","volume":"19","author":"J.W. Cooley","year":"1965","unstructured":"Cooley, J.W., Tukey, J.W.: An Algorithm for Machine Calculation of Complex Fourier Series. Mathematics of Computation\u00a019, 297\u2013301 (1965)","journal-title":"Mathematics of Computation"},{"key":"4_CR11","volume-title":"Computer Solution of Linear Algebraic Systems","author":"G. Forsythe","year":"1967","unstructured":"Forsythe, G., Moler, C.B.: Computer Solution of Linear Algebraic Systems. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"4_CR12","unstructured":"Gamboa, R.A.: The Correctness of the Fast Fourier Transform: A Structural Proof in ACL2. Formal Methods in System Design, Special Issue on UNITY (January 2002)"},{"key":"4_CR13","first-page":"563","volume-title":"AFIPS Fall Joint Computer Conference","author":"W.M. Gentleman","year":"1966","unstructured":"Gentleman, W.M., Sande, G.: Fast Fourier Transforms - For Fun and Profit. In: AFIPS Fall Joint Computer Conference, vol.\u00a029, pp. 563\u2013578. Spartan Books, Washington (1966)"},{"key":"4_CR14","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"1\/2","key":"4_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF01384233","volume":"5","author":"J.R. Harrison","year":"1994","unstructured":"Harrison, J.R.: Constructing the Real Numbers in HOL. Formal Methods in System Design\u00a05(1\/2), 35\u201359 (1994)","journal-title":"Formal Methods in System Design"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J.R. Harrison","year":"1999","unstructured":"Harrison, J.R.: A Machine-Checked Theory of Floating-Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1008712907154","volume":"16","author":"J.R. Harrison","year":"2000","unstructured":"Harrison, J.R.: Floating-Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design\u00a016(3), 271\u2013305 (2000)","journal-title":"Formal Methods in System Design"},{"key":"4_CR18","unstructured":"Harrison, J.R.: Complex Quantifier Elimination in HOL. In: Supplemental Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 159\u2013174 (September 2001)"},{"issue":"4","key":"4_CR19","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1145\/321607.321613","volume":"17","author":"T. Kaneko","year":"1970","unstructured":"Kaneko, T., Liu, B.: Accumulation of Round-Off Error in Fast Fourier Transforms. Journal of Association for Computing Machinery\u00a017(4), 637\u2013654 (1970)","journal-title":"Journal of Association for Computing Machinery"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Keding, H., Willems, M., Coors, M., Meyr, H.: FRIDGE: A Fixed-Point Design and Simulation Environment. In: Proceedings Design Automation and Test in Europe Conference, Paris, France, pp. 429\u2013435 (February 1998)","DOI":"10.1109\/DATE.1998.655893"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Liu, B., Kaneko, T.: Roundoff Error in Fast Fourier Transforms (Decimation in Time). In: Proceedings of the IEEE (Proceedings Letters), pp. 991\u2013992 (June 1975)","DOI":"10.1109\/PROC.1975.9873"},{"key":"4_CR22","unstructured":"Mathworks, Inc. Fixed-Point Blockset User\u2019s Guide (ver. 2.0) (1999)"},{"key":"4_CR23","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569845","volume-title":"Higher Order Logic and Hardware Verification","author":"T. Melham","year":"1993","unstructured":"Melham, T.: Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science, vol.\u00a031. Cambridge University Press, Cambridge (1993)"},{"issue":"6","key":"4_CR24","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1145\/197320.197356","volume":"16","author":"J. Misra","year":"1994","unstructured":"Misra, J.: Powerlists: A Structure for Parallel Recursion. ACM Transactions on Programming Languages and Systems\u00a016(6), 1737\u20131767 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR25","volume-title":"Discrete-Time Signal Processing","author":"A.V. Oppenheim","year":"1989","unstructured":"Oppenheim, A.V., Schafer, R.W.: Discrete-Time Signal Processing. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"8","key":"4_CR26","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/PROC.1972.8820","volume":"60","author":"A.V. Oppenheim","year":"1972","unstructured":"Oppenheim, A.V., Weinstein, C.J.: Effects of Finite Register Length in Digital Filtering and the Fast Fourier Transform. Proceedings of the IEEE\u00a060(8), 957\u2013976 (1972)","journal-title":"Proceedings of the IEEE"},{"key":"4_CR27","unstructured":"Cadence Design Systems, Inc. Signal Processing WorkSystem (SPW) User\u2019s Guide, USA (July 1999)"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1109\/TASSP.1976.1162875","volume":"24","author":"T. Thong","year":"1976","unstructured":"Thong, T., Liu, B.: Fixed-Point Fast Fourier Transform Error Analysis. IEEE Transactions on Acoustics, Speech, and Signal Processing, ASSP\u00a024(6), 563\u2013573 (1976)","journal-title":"IEEE Transactions on Acoustics, Speech, and Signal Processing, ASSP"},{"issue":"3","key":"4_CR29","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/TAU.1969.1162049","volume":"AU-17","author":"C.J. Weinstein","year":"1969","unstructured":"Weinstein, C.J.: Roundoff Noise in Floating Point Fast Fourier Transform Computation. IEEE Transactions on Audio and Electroacoustics\u00a0AU-17(3), 209\u2013215 (1969)","journal-title":"IEEE Transactions on Audio and Electroacoustics"},{"issue":"2","key":"4_CR30","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1109\/TAU.1969.1162035","volume":"AU-17","author":"P.D. Welch","year":"1969","unstructured":"Welch, P.D.: A Fixed-Point Fast Fourier Transform Error Analysis. IEEE Transactions on Audio and Electroacoustics\u00a0AU-17(2), 151\u2013157 (1969)","journal-title":"IEEE Transactions on Audio and Electroacoustics"},{"key":"4_CR31","volume-title":"Rounding Errors in Algebraic Processes","author":"J.H. Wilkinson","year":"1963","unstructured":"Wilkinson, J.H.: Rounding Errors in Algebraic Processes. Prentice-Hall, Englewood Cliffs (1963)"},{"key":"4_CR32","unstructured":"Xilinx, Inc. High-Performance 16-Point Complex FFT\/IFFT V1.0.5, Product Specification, USA (July 2000), http:\/\/xilinx.com\/ipcenter"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:56:49Z","timestamp":1740218209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}