{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:42:52Z","timestamp":1761561772689},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T00:00:00Z","timestamp":1371945600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10009-013-0279-9","type":"journal-article","created":{"date-parts":[[2013,6,22]],"date-time":"2013-06-22T14:22:17Z","timestamp":1371910937000},"page":"175-190","source":"Crossref","is-referenced-by-count":8,"title":["A bit too precise? Verification of quantized digital filters"],"prefix":"10.1007","volume":"16","author":[{"given":"Arlen","family":"Cox","sequence":"first","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,6,23]]},"reference":[{"issue":"4","key":"279_CR1","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1016\/j.jal.2006.11.001","volume":"5","author":"B Akbarpour","year":"2007","unstructured":"Akbarpour, B., Tahar, S.: Error analysis of digital filters using HOL theorem proving? J. Appl. Log. 5(4), 651\u2013666 (2007)","journal-title":"J. Appl. Log."},{"key":"279_CR2","unstructured":"Alegre, F., Feron, E., Pande, S.: Using ellipsoidal domains to analyze control systems software. CoRR, abs\/0909.1977 (2009)"},{"key":"279_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3):243\u2013277 (2013)","DOI":"10.1007\/s10817-012-9246-5"},{"key":"279_CR4","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) Format Version 20071012 (2007)"},{"key":"279_CR5","unstructured":"Biere, A., Heljanko, K.: Hardware model checking competition. In: FMCAD (2011)"},{"key":"279_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software (invited chapter). In: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of LNCS, pp. 85\u2013108. Springer, Berlin (2005)","DOI":"10.1007\/3-540-36377-7_5"},{"key":"279_CR7","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI), vol. 6538, pp. 70\u201387. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"279_CR8","doi-asserted-by":"crossref","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Computer-Aided Verification (CAV), pp. 24\u201340 (2010)","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"279_CR9","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Formal Methods in Computer Aided Design (FMCAD), pp. 69\u201376 (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"issue":"1","key":"279_CR10","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"279_CR11","doi-asserted-by":"crossref","unstructured":"Cox, A., Sankaranarayanan, S., Chang, B.-Y.E.: A bit too precise? Bounded verification of quantized digital filters. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 33\u201347 (2012)","DOI":"10.1007\/978-3-642-28756-5_4"},{"issue":"3","key":"279_CR12","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"279_CR13","unstructured":"de Figueiredo, L.H., Stolfi, J.: Self-validated numerical methods and applications. In: Brazilian Mathematics Colloquium monograph. IMPA, Rio de Janeiro, Brazil (1997)"},{"key":"279_CR14","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"279_CR15","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Formal Methods in Computer Aided Design (FMCAD), pp. 125\u2013134. FMCAD Inc (2011)"},{"key":"279_CR16","doi-asserted-by":"crossref","unstructured":"Fang, C., Rutenbar, R., Chen, T.: Fast, accurate static analysis for fixed-point finite-precision effects in DSP designs. In: International Conference on Computer-Aided Design (ICCAD), pp. 275\u2013282 (2003)","DOI":"10.1109\/ICCAD.2003.159701"},{"key":"279_CR17","doi-asserted-by":"crossref","unstructured":"Feret, J.: Static analysis of digital filters. In: Programming Languages and Systems 2986, 33\u201348 (2004)","DOI":"10.1007\/978-3-540-24725-8_4"},{"issue":"3\u20134","key":"279_CR18","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT 1(3\u20134), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"279_CR19","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 232\u2013247 (2011)","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"279_CR20","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT), vol. 7317, pp. 157\u2013171. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"279_CR21","doi-asserted-by":"crossref","unstructured":"Kinsman, A.B., Nicolici, N.: Finite precision bit-width allocation using SAT-modulo theory. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE \u201909, p. 11061111. European Design and Automation Association (2009)","DOI":"10.1109\/DATE.2009.5090829"},{"issue":"10","key":"279_CR22","doi-asserted-by":"crossref","first-page":"1990","DOI":"10.1109\/TCAD.2006.873887","volume":"25","author":"D Lee","year":"2006","unstructured":"Lee, D., Gaffar, A., Cheung, R., Mencer, O., Luk, W., Constantinides, G.: Accuracy-guaranteed bit-width optimization. IEEE Trans. CAD Integr. Circuits Syst. 25(10), 1990\u20132000 (2006)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"279_CR23","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Computer-Aided Verification (CAV), pp. 1\u201313 (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"279_CR24","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Compositional analysis of floating-point linear numerical filters. In: Computer-Aided Verification (CAV), vol.\u00a03576, pp. 199\u2013212 (2005)","DOI":"10.1007\/11513988_21"},{"key":"279_CR25","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Computer-Aided Verification (CAV), pp. 570\u2013583 (2009)","DOI":"10.1007\/978-3-642-02658-4_42"},{"key":"279_CR26","volume-title":"Signals & Systems","author":"AV Oppenheim","year":"1997","unstructured":"Oppenheim, A.V., Willsky, A.S., Nawab, S.H.: Signals & Systems, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"issue":"8","key":"279_CR27","doi-asserted-by":"crossref","first-page":"1177","DOI":"10.1109\/TCAD.2010.2049154","volume":"29","author":"Y Pang","year":"2010","unstructured":"Pang, Y., Radecka, K., Zilic, Z.: Optimization of imprecise circuits represented by taylor series and real-valued polynomials. IEEE Trans. CAD Integr. Circuits Syst. 29(8), 1177\u20131190 (2010)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"279_CR28","doi-asserted-by":"crossref","unstructured":"Pang, Y., Radecka, K., Zilic, Z.: An efficient hybrid engine to perform range analysis and allocate integer bit-widths for arithmetic circuits. In: Asia South Pacific Design Automation Conference (ASP-DAC), pp. 455\u2013460 (2011)","DOI":"10.1109\/ASPDAC.2011.5722233"},{"key":"279_CR29","unstructured":"Smith, J.O.: Introduction to Digital Filters: With Audio Applications. W3K Publishing. http:\/\/books.w3k.org\/ , ISBN 978-0-9745607-1-7 (2007)"},{"issue":"12","key":"279_CR30","doi-asserted-by":"crossref","first-page":"3087","DOI":"10.1109\/78.476465","volume":"43","author":"W Sung","year":"1995","unstructured":"Sung, W., Kum, K.: Simulation-based word-length optimization method for fixed-point digital signal processing systems. IEEE Trans. Signal Process. 43(12), 3087\u20133090 (1995)","journal-title":"IEEE Trans. Signal Process."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0279-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0279-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0279-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T22:34:43Z","timestamp":1563230083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0279-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,23]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["279"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0279-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,23]]}}}