{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T16:03:35Z","timestamp":1725984215848},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319968117"},{"type":"electronic","value":"9783319968124"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-96812-4_8","type":"book-chapter","created":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T04:26:41Z","timestamp":1531801601000},"page":"87-103","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Coq Formalization of Digital Filters"],"prefix":"10.1007","author":[{"given":"Diane","family":"Gallois-Wong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvie","family":"Boldo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thibault","family":"Hilaire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"4","key":"8_CR1","doi-asserted-by":"publisher","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. Logic 5(4), 651\u2013666 (2007). 4th International Workshop on Computational Models of Scientific Reasoning and Applications","journal-title":"J. Appl. Logic"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Hilaire, T., Lopez, B.: Reliable implementation of linear filters with fixed-point arithmetic. In: Proceedings of IEEE Workshop on Signal Processing Systems (SiPS) (2013)","DOI":"10.1109\/SiPS.2013.6674540"},{"key":"8_CR3","unstructured":"Siddique, U., Mahmoud, M.Y., Tahar, S.: Formal analysis of discrete-time systems using z-transform. J. Appl. Logic, 1\u201332 (2018, accepted). Elsevier"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10703-005-2256-8","volume":"27","author":"B Akbarpour","year":"2005","unstructured":"Akbarpour, B., Tahar, S., Dekdouk, A.: Formalization of fixed-point arithmetic in HOL. Formal Methods Syst. Des. 27(1), 173\u2013200 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/978-3-662-49674-9_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Park","year":"2016","unstructured":"Park, J., Pajic, M., Lee, I., Sokolsky, O.: Scalable verification of linear controller software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 662\u2013679. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_43"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-662-54577-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Park","year":"2017","unstructured":"Park, J., Pajic, M., Sokolsky, O., Lee, I.: Automatic verification of finite precision implementations of linear controllers. In: Legay, A., Margaria, T. (eds.) TACAS 2017 Part I. LNCS, vol. 10205, pp. 153\u2013169. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_9"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33\u201348. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24725-8_4"},{"key":"8_CR8","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. TTCS. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"8_CR9","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual (2017)"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"8_CR11","volume-title":"Discrete-Time Signal Processing","author":"AV Oppenheim","year":"1999","unstructured":"Oppenheim, A.V., Schafer, R.W., Buck, J.R.: Discrete-Time Signal Processing, 2nd edn. Prentice-Hall Inc., Upper Saddle River (1999)","edition":"2"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-319-08970-6_31","volume-title":"Interactive Theorem Proving","author":"U Siddique","year":"2014","unstructured":"Siddique, U., Mahmoud, M.Y., Tahar, S.: On the formalization of Z-transform in HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 483\u2013498. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08970-6_31"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"issue":"2","key":"8_CR14","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1109\/PROC.1986.13458","volume":"74","author":"A Fettweiss","year":"1986","unstructured":"Fettweiss, A.: Wave digital filters: theory and practice. Proc. IEEE 74(2), 270\u2013327 (1986)","journal-title":"Proc. IEEE"},{"key":"8_CR15","volume-title":"Digital Control and Estimation, a Unified Approach","author":"R Middleton","year":"1990","unstructured":"Middleton, R., Goodwin, G.: Digital Control and Estimation, a Unified Approach. Prentice-Hall International Editions, Upper Saddle River (1990)"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1109\/TCSII.2004.842416","volume":"52","author":"G Li","year":"2005","unstructured":"Li, G., Wan, C., Bi, G.: An improved $$\\rho $$\u03c1-DFIIt structure for digital filters with minimum roundoff noise. IEEE Trans. Circ. Syst. 52(4), 199\u2013203 (2005)","journal-title":"IEEE Trans. Circ. Syst."},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/0005-1098(87)90115-4","volume":"23","author":"H Hanselmann","year":"1987","unstructured":"Hanselmann, H.: Implementation of digital controllers - a survey. Automatica 23(1), 7\u201332 (1987)","journal-title":"Automatica"},{"key":"8_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2039-1","volume-title":"Parametrizations in Control, Estimation and Filtering Probems","author":"M Gevers","year":"1993","unstructured":"Gevers, M., Li, G.: Parametrizations in Control, Estimation and Filtering Probems. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/978-1-4471-2039-1"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0167-6911(92)90064-Y","volume":"19","author":"V Balakrishnan","year":"1992","unstructured":"Balakrishnan, V., Boyd, S.: On computing the worst-case peak gain of linear systems. Syst. Control Lett. 19, 265\u2013269 (1992)","journal-title":"Syst. Control Lett."},{"issue":"1","key":"8_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6911(87)90002-8","volume":"9","author":"SP Boyd","year":"1987","unstructured":"Boyd, S.P., Doyle, J.: Comparison of peak and RMS gains for discrete-time systems. Syst. Control Lett. 9(1), 1\u20136 (1987)","journal-title":"Syst. Control Lett."},{"key":"8_CR21","volume-title":"Linear Systems","author":"T Kailath","year":"1980","unstructured":"Kailath, T.: Linear Systems. Prentice-Hall, Upper Saddle River (1980)"},{"issue":"54","key":"8_CR22","doi-asserted-by":"publisher","first-page":"1765","DOI":"10.1109\/TCSI.2007.902408","volume":"8","author":"T Hilaire","year":"2007","unstructured":"Hilaire, T., Chevrel, P., Whidborne, J.: A unifying framework for finite wordlength realizations. IEEE Trans. Circ. Syst. 8(54), 1765\u20131774 (2007)","journal-title":"IEEE Trans. Circ. Syst."},{"key":"8_CR23","volume-title":"Computer Arithmetic and Formal Proofs","author":"S Boldo","year":"2017","unstructured":"Boldo, S., Melquiond, G.: Computer Arithmetic and Formal Proofs. ISTE Press - Elsevier, London (2017)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96812-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T04:30:34Z","timestamp":1531801834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96812-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319968117","9783319968124"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96812-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}