{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T01:22:19Z","timestamp":1771636939986,"version":"3.50.1"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,5,20]],"date-time":"2016-05-20T00:00:00Z","timestamp":1463702400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["475647\/2013-0"],"award-info":[{"award-number":["475647\/2013-0"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004916","name":"FAPEAM","doi-asserted-by":"crossref","award":["062.01722\/2014"],"award-info":[{"award-number":["062.01722\/2014"]}],"id":[{"id":"10.13039\/501100004916","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Braz Comput Soc"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1186\/s13173-016-0041-8","type":"journal-article","created":{"date-parts":[[2016,5,21]],"date-time":"2016-05-21T19:39:57Z","timestamp":1463859597000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Bounded model checking for fixed-point digital filters"],"prefix":"10.1186","volume":"22","author":[{"given":"Renato B.","family":"Abreu","sequence":"first","affiliation":[]},{"given":"Mikhail Y. R.","family":"Gadelha","sequence":"additional","affiliation":[]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[]},{"given":"Eddie B.","family":"de Lima Filho","sequence":"additional","affiliation":[]},{"suffix":"Jr","given":"Waldir S.","family":"da Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,20]]},"reference":[{"key":"41_CR1","volume-title":"IEEE standard for floating-point arithmetic (IEEE Std 754-2008)","author":"Institute of Electrical and Electronics Engineers","year":"2008","unstructured":"Institute of Electrical and Electronics Engineers (2008) IEEE standard for floating-point arithmetic (IEEE Std 754-2008). IEEE, New York."},{"key":"41_CR2","volume-title":"Digital signal processing: principles, algorithms, and applications","author":"JG Proakis","year":"1996","unstructured":"Proakis JG, Manolakis DG (1996) Digital signal processing: principles, algorithms, and applications. Prentice Hall, Upper Saddle River."},{"issue":"6","key":"41_CR3","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/TCT.1971.1083367","volume":"18","author":"SR Parker","year":"1971","unstructured":"Parker SR, Hess SF (1971) Limit-cycle oscillations in digital filters. IEEE Trans Circuit Theory 18(6): 687\u2013697.","journal-title":"IEEE Trans Circuit Theory"},{"issue":"11","key":"41_CR4","doi-asserted-by":"publisher","first-page":"2400","DOI":"10.1109\/78.97995","volume":"39","author":"P Bauer","year":"1991","unstructured":"Bauer P, Leclerc LJ (1991) A computer-aided test for the absence of limit cycles in fixed-point digital filters. IEEE Trans Signal Process 39(11): 2400\u20132410.","journal-title":"IEEE Trans Signal Process"},{"issue":"6","key":"41_CR5","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF01204681","volume":"14","author":"EM Shafic","year":"1995","unstructured":"Shafic EM, Sandberg IW (1995) A study of bounds on limit cycles in digital filters. Circ Syst Signal Process 14(6): 725\u2013734.","journal-title":"Circ Syst Signal Process"},{"issue":"3","key":"41_CR6","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1109\/LSP.2005.862606","volume":"13","author":"J Campo","year":"2006","unstructured":"Campo J, Cruz-Roldan F, Utrilla-Manso M (2006) Tighter limit cycle bounds for digital filters. IEEE Signal Process Lett 13(3): 149\u2013152.","journal-title":"IEEE Signal Process Lett"},{"issue":"6","key":"41_CR7","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1109\/TASSP.1976.1162863","volume":"24","author":"TACM Claasen","year":"1976","unstructured":"Claasen TACM, Mecklenbrauker WFG, Peek JBH (1976) Effects of quantization and overflow in recursive digital filters. IEEE Trans Acoust Speech Signal Process 24(6): 517\u2013529.","journal-title":"IEEE Trans Acoust Speech Signal Process"},{"issue":"3","key":"41_CR8","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1109\/TCS.1987.1086118","volume":"34","author":"PP Vaidyanathan","year":"1987","unstructured":"Vaidyanathan PP, Liu V (1987) An improved sufficient condition for absence of limit cycles in digital filters. IEEE Trans Circuits Syst 34(3): 319\u2013322.","journal-title":"IEEE Trans Circuits Syst"},{"issue":"3","key":"41_CR9","doi-asserted-by":"publisher","first-page":"1433","DOI":"10.1007\/s00034-012-9520-0","volume":"32","author":"CK Ahn","year":"2013","unstructured":"Ahn CK (2013) IOSS criterion for the absence of limit cycles in interfered digital filters employing saturation overflow arithmetic. Circ Syst Signal Process 32(3): 1433\u20131441.","journal-title":"Circ Syst Signal Process"},{"issue":"1","key":"41_CR10","first-page":"4650","volume":"55","author":"M Kawamata","year":"2008","unstructured":"Kawamata M (2008) On the absence of limit cycles in state-space digital filters with minimum L2-sensitivity. IEEE Trans Circuits Syst II Exp Briefs 55(1): 4650.","journal-title":"IEEE Trans Circuits Syst II Exp Briefs"},{"issue":"9","key":"41_CR11","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1016\/j.aeue.2010.12.001","volume":"65","author":"CK Ahn","year":"2011","unstructured":"Ahn CK (2011) Criterion for the elimination of overflow oscillations in fixed-point digital filters with saturation arithmetic and external disturbance. Int J Electron Commun 65(9): 750\u2013752.","journal-title":"Int J Electron Commun"},{"key":"41_CR12","first-page":"57","volume-title":"IEEE International Symposium on Circuits and Systems, Geneva, May 2000. Proceedings of ISCAS 2000, vol 4","author":"GA Constantinides","year":"2000","unstructured":"Constantinides GA, Cheung PYK, Luk W (2000) Roundoff-noise shaping in filter design In: IEEE International Symposium on Circuits and Systems, Geneva, May 2000. Proceedings of ISCAS 2000, vol 4, 57\u201360.. IEEE, Geneva, Switzerland."},{"key":"41_CR13","first-page":"169","volume-title":"4th International Conference on Computer Recognition Systems, Rydzyna Castle, Poland, May 2005. Advances in Soft Computing, vol 30","author":"N Henzel","year":"2005","unstructured":"Henzel N (2005) Digital filter design with constraints in time and frequency domains In: 4th International Conference on Computer Recognition Systems, Rydzyna Castle, Poland, May 2005. Advances in Soft Computing, vol 30, 169\u2013176.. Springer, Rydzyna Castle, Poland."},{"key":"41_CR14","unstructured":"SYNOPSYS\u00ae; (2013) SPW. \n                    http:\/\/www.synopsys.com\/Systems\/BlockDesign\/DigitalSignalProcessing\/Pages\/Signal-Processing.aspx\n                    \n                  . Accessed 20 Nov 2013."},{"key":"41_CR15","unstructured":"MathWorks\u00ae; (2013) Fixed-point designer. \n                    http:\/\/www.mathworks.com\/products\/simfixed\n                    \n                  . Accessed 20 Nov 2013."},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Wang CC, Shi C, Brodersen RW, Markovi\u0107 D (2011) An automated fixed-point optimization tool in MATLAB XSG\/SynDSP environment. ISRN Signal Process: 1\u201317.","DOI":"10.5402\/2011\/414293"},{"issue":"12","key":"41_CR17","doi-asserted-by":"publisher","first-page":"3087","DOI":"10.1109\/78.476465","volume":"43","author":"W Sung","year":"1995","unstructured":"Sung W, Kum KL (1995) Simulation-based word-length optimization method for fixed-point digital signal processing systems. IEEE Trans Signal Process 43(12): 3087\u20133090.","journal-title":"IEEE Trans Signal Process"},{"key":"41_CR18","first-page":"1944","volume-title":"European Signal Processing Conference, Barcelona, Spain, September 2011. Proceedings of EUSIPCO 2011","author":"HN Nguyen","year":"2011","unstructured":"Nguyen HN, Menard D, Sentieys O (2011) Novel algorithms for word-length optimization In: European Signal Processing Conference, Barcelona, Spain, September 2011. Proceedings of EUSIPCO 2011, 1944\u20131948.. EURASIP, Barcelona, Spain."},{"issue":"10","key":"41_CR19","doi-asserted-by":"publisher","first-page":"3197","DOI":"10.1109\/TCSI.2008.923279","volume":"55","author":"D Menard","year":"2008","unstructured":"Menard D, Rocher R, Sentieys O (2008) Analytical fixed-point accuracy evaluation in linear time-invariant systems. IEEE Trans Circ Syst I Reg Papers 55(10): 3197\u20133208.","journal-title":"IEEE Trans Circ Syst I Reg Papers"},{"key":"41_CR20","first-page":"33","volume-title":"18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, April 2012. Lecture Notes in Computer Science, vol 7214","author":"A Cox","year":"2012","unstructured":"Cox A, Sankaranarayanan S, Chang BYE (2012) A bit too precise? Bounded verification of quantized digital filters In: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, April 2012. Lecture Notes in Computer Science, vol 7214, 33\u201347.. Springer, Heidelberg."},{"issue":"2","key":"41_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10009-013-0279-9","volume":"16","author":"A Cox","year":"2014","unstructured":"Cox A, Sankaranarayanan S, Chang BYE (2014) A bit too precise? Verification of quantized digital filters. Softw Tools Technol Transfer 16(2): 175\u2013190.","journal-title":"Softw Tools Technol Transfer"},{"key":"41_CR22","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere A (2009) Bounded model checking In: Handbook of Satisfiability.. IOS Press, Amsterdam, The Netherlands."},{"key":"41_CR23","volume-title":"Handbook of Satisfiability","author":"CW Barrett","year":"2009","unstructured":"Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories In: Handbook of Satisfiability.. IOS Press, Amsterdam, The Netherlands."},{"issue":"4","key":"41_CR24","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro L, Fischer B, Marques-Silva J (2012) SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans Softw Eng 38(4): 957\u2013974.","journal-title":"IEEE Trans Softw Eng"},{"key":"41_CR25","first-page":"331","volume-title":"International Conference on Software Engineering, Honolulu, USA, May 2011. Proceedings of ICSE 2011","author":"L Cordeiro","year":"2011","unstructured":"Cordeiro L, Fischer B (2011) Verifying multi-threaded software using SMT-based context-bounded model checking In: International Conference on Software Engineering, Honolulu, USA, May 2011. Proceedings of ICSE 2011, 331\u2013340.. ACM, Honolulu, USA."},{"key":"41_CR26","first-page":"1","volume-title":"XXXI Brazilian Telecommunications Simposyum, Fortaleza, Brazil, September 2013. Proceedings of SBrT 2013","author":"RB Abreu","year":"2013","unstructured":"Abreu RB, Cordeiro LC, Filho EBL (2013) Verifying fixed-point digital filters using SMT-based bounded model checking In: XXXI Brazilian Telecommunications Simposyum, Fortaleza, Brazil, September 2013. Proceedings of SBrT 2013, 1\u20135.. Sociedade Brasileira de Telecomunica\u00e7\u00f5es, Fortaleza, Brazil."},{"key":"41_CR27","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1109\/IECON.2014.7048514","volume-title":"40th Annual Conference of the IEEE Industrial Electronics Society, Dallas, UA, October 2014. Proceedings of IECON 2014","author":"I Bessa","year":"2014","unstructured":"Bessa I, Abreu R, Chaves Filho JE, Cordeiro L (2014) SMT-based bounded model checking of fixed-point digital controllers In: 40th Annual Conference of the IEEE Industrial Electronics Society, Dallas, UA, October 2014. Proceedings of IECON 2014, 295\u2013301.. IEEE, Dallas, USA."},{"key":"41_CR28","first-page":"168","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, March 2004. Lecture Notes in Computer Science, vol 2988","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, March 2004. Lecture Notes in Computer Science, vol 2988, 168\u2013176.. Springer, Heidelberg."},{"key":"41_CR29","volume-title":"Discrete-time signal processing","author":"AV Oppenheim","year":"1999","unstructured":"Oppenheim AV, Schafer RW, Buck JR (1999) Discrete-time signal processing. 2nd ed. Prentice Hall, Upper Saddle River."},{"key":"41_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2039-1","volume-title":"Parametrizations in control, estimation, and filtering problems: accuracy aspects","author":"M Gevers","year":"1993","unstructured":"Gevers M, Li G (1993) Parametrizations in control, estimation, and filtering problems: accuracy aspects. Springer-Verlag, London."},{"issue":"4","key":"41_CR31","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1109\/TASSP.1978.1163114","volume":"26","author":"W Mills","year":"1978","unstructured":"Mills W, Mullis C, Roberts RA (1978) Digital filter realizations without overflow oscillations. IEEE Trans Acoust Speech Signal Process 26(4): 334\u2013338.","journal-title":"IEEE Trans Acoust Speech Signal Process"},{"key":"41_CR32","unstructured":"Hilaire T (2011) Towards tools and methodology for the fixed-point implementation of linear filters In: Digital Signal Processing Workshop and Signal Processing Education Workshop, Sedona, USA, January 2011. Proceedings of DSP\/SPE 2011, 488493."},{"issue":"3","key":"41_CR33","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1109\/TAU.1968.1162002","volume":"AU-16","author":"LB Jackson","year":"1968","unstructured":"Jackson LB, Kaiser JF, McDonald HS (1968) An approach to the implementation of digital filters. IEEE Trans Audio ElectroacoustAU-16(3): 413\u2013421.","journal-title":"IEEE Trans Audio Electroacoust"},{"issue":"11","key":"41_CR34","first-page":"851","volume":"36","author":"J Dattorro","year":"1988","unstructured":"Dattorro J (1988) The implementation of recursive digital filters for high-fidelity audio. J Audio Eng Soc 36(11): 851\u2013878.","journal-title":"J Audio Eng Soc"},{"issue":"5","key":"41_CR35","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1109\/TAC.1972.1100120","volume":"17","author":"T Brubaker","year":"1972","unstructured":"Brubaker T, Gowdy J (1972) Limit cycles in digital filters. IEEE Trans Autom Control 17(5): 675\u2013677.","journal-title":"IEEE Trans Autom Control"},{"issue":"1","key":"41_CR36","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 (1987) Implementation of digital controllers\u2014a survey. Automatica 23(1): 7\u201332.","journal-title":"Automatica"},{"issue":"1","key":"41_CR37","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/TCSII.2007.907757","volume":"55","author":"S Yamaki","year":"2008","unstructured":"Yamaki S, Abe M, Kawamata M (2008) On the absence of limit cycles in state-space digital filters with minimum L\n                           2-sensitivity. IEEE Trans Circuits Syst II Exp Briefs 55(1): 46\u201350.","journal-title":"IEEE Trans Circuits Syst II Exp Briefs"},{"key":"41_CR38","first-page":"904","volume-title":"IEEE International Conference on Acoustics, Speech, and Signal Processing, Dallas, USA, April 1987. Proceedings of ICASSP 1987, vol 12","author":"E Auer","year":"1987","unstructured":"Auer E (1987) Digital filter structures free of limit cycles In: IEEE International Conference on Acoustics, Speech, and Signal Processing, Dallas, USA, April 1987. Proceedings of ICASSP 1987, vol 12, 904\u2013907.. IEEE, Dallas, USA."},{"key":"41_CR39","unstructured":"Ritzerfeld JHF, Mollova GS (1997) Controlled rounding in low noise digital filter structures In: ProRISC Workshop on Circuits, Systems and Signal Processing, Mierlo, The Netherlands, September 1987. Proceedings of the ProRISC Workshop on Circuits, Systems and Signal Processing, 433\u2013437."},{"issue":"9","key":"41_CR40","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1109\/TCS.1985.1085796","volume":"32","author":"H Kwan","year":"1985","unstructured":"Kwan H (1985) A multi-output second-order digital filter without limit cycle oscillations. IEEE Trans Circuits Syst 32(9): 974\u2013975.","journal-title":"IEEE Trans Circuits Syst"},{"issue":"4","key":"41_CR41","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1049\/iet-cds:20070198","volume":"2","author":"JA L\u00f3pez","year":"2008","unstructured":"L\u00f3pez JA, Caffarena G, Carreras C, Nieto-Taladriz O (2008) Fast and accurate computation of the roundoff noise of linear time-invariant systems. IET Circ Devices Syst 2(4): 393\u2013408.","journal-title":"IET Circ Devices Syst"},{"issue":"2","key":"41_CR42","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/TAU.1970.1162084","volume":"18","author":"L Jackson","year":"1970","unstructured":"Jackson L (1970) Roundoff-noise analysis for fixed-point digital filters realized in cascade or parallel form. IEEE Trans Audio Electroacoust 18(2): 107\u2013122.","journal-title":"IEEE Trans Audio Electroacoust"},{"key":"41_CR43","first-page":"1019","volume-title":"15th European Signal Processing Conference, Poznan, Poland, September 2007. Proceedings of EUSIPCO 2007","author":"T Hilaire","year":"2007","unstructured":"Hilaire T, M\u00e9nard D, Sentieys O (2007) Roundoff noise analysis of finite word length realizations with the implicit state-space framework In: 15th European Signal Processing Conference, Poznan, Poland, September 2007. Proceedings of EUSIPCO 2007, 1019\u20131023.. EURASIP, Poznan, Poland."},{"key":"41_CR44","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments, Philadelphia, USA, January 2012. Lecture Notes in Computer Science, Vol 7152","author":"F Merz","year":"2012","unstructured":"Merz F, Falke S, Sinz C (2012) LLBMC: Bounded model checking of C and C++ programs using a compiler IR In: Verified Software: Theories, Tools, Experiments, Philadelphia, USA, January 2012. Lecture Notes in Computer Science, Vol 7152, 146\u2013161.. Springer, Heidelberg."},{"key":"41_CR45","doi-asserted-by":"crossref","unstructured":"Cordeiro L, Morse J, Nicole D, Fischer B (2012) 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, March 2012. Lecture Notes in Computer Science, vol 7214, 534\u2013537.. Springer, Heidelberg.","DOI":"10.1007\/978-3-642-28756-5_42"},{"key":"41_CR46","first-page":"619","volume-title":"19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy, March 2013. Lecture Notes in Computer Science, vol 7795","author":"J Morse","year":"2013","unstructured":"Morse J, Cordeiro L, Nicole D, Fischer B (2013) Handling unbounded loops with ESBMC 1.20 In: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy, March 2013. Lecture Notes in Computer Science, vol 7795, 619\u2013622.. Springer, Heidelberg."},{"key":"41_CR47","first-page":"405","volume-title":"20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, France, April 2014. Lecture Notes in Computer Science, vol 8413","author":"J Morse","year":"2014","unstructured":"Morse J, Ramalho M, Cordeiro L, Nicole D, Fischer B (2014) ESBMC 1.22 - (Competition Contribution) In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, France, April 2014. Lecture Notes in Computer Science, vol 8413, 405\u2013407.. Springer, Heidelberg."},{"key":"41_CR48","first-page":"127","volume-title":"International Workshop on Formal Aspects of Component Software, Macao, China, October 2005, vol 160. Proceedings of FACS 2005","author":"J Carlson","year":"2005","unstructured":"Carlson J, Hakansson J, Pettersson P (2005) SaveCCM: An analysable component model for real-time systems In: International Workshop on Formal Aspects of Component Software, Macao, China, October 2005, vol 160. Proceedings of FACS 2005, 127\u2013140.. Electr. Notes Theor. Comput. Sci.,Macao China."},{"issue":"3","key":"41_CR49","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"T Tripakis","year":"2005","unstructured":"Tripakis T, Yovine S, Bouajjani A (2005) Checking timed Buchi automata emptiness efficiently. Form Methods Syst Des 26(3): 267\u2013292.","journal-title":"Form Methods Syst Des"},{"key":"41_CR50","doi-asserted-by":"publisher","DOI":"10.1007\/b95112","volume-title":"Coloured Petri nets: modelling and validation of concurrent systems","author":"K Jensen","year":"2009","unstructured":"Jensen K, Kristensen LM (2009) Coloured Petri nets: modelling and validation of concurrent systems. Springer, Berlin, Germany."},{"key":"41_CR51","first-page":"24","volume-title":"22nd International Conference on Computer-Aided Verification, Edinburgh, July 210. Lecture Notes in Computer Science, vol 6174","author":"RK Brayton","year":"2010","unstructured":"Brayton RK, Mishchenko A (2010) ABC: An academic industrial-strength verification tool In: 22nd International Conference on Computer-Aided Verification, Edinburgh, July 210. Lecture Notes in Computer Science, vol 6174, 24\u201340.. Springer, Edinburgh, Scotland."},{"key":"41_CR52","first-page":"126","volume-title":"22nd International SPIN Symposium on Model Checking of Software, Stellenbosch, South Africa. Lecture Notes in Computer Science, vol 9232","author":"H Ismail","year":"2015","unstructured":"Ismail H, Bessa I, Cordeiro L, de Lima Filho EB, Chaves Filho E (2015) DSVerifier: A bounded model checking tool for digital systems In: 22nd International SPIN Symposium on Model Checking of Software, Stellenbosch, South Africa. Lecture Notes in Computer Science, vol 9232, 126\u2013131.. Springer, Heidelberg."},{"key":"41_CR53","unstructured":"MathWorks\u00ae; (2013) Open filter design and analysis tool. \n                    http:\/\/www.mathworks.com\/help\/dsp\/ref\/fdatool.html\n                    \n                  . Accessed 21 Nov 2013."},{"key":"41_CR54","first-page":"656","volume-title":"Design Automation Conference, Anaheim, USA, June 2003. Proceeding of the Design Automation Conference","author":"J Carletta","year":"2003","unstructured":"Carletta J, Veillette R, Krach F, Fang Z (2003) Determining appropriate precisions for signals in fixed-point IIR filters In: Design Automation Conference, Anaheim, USA, June 2003. Proceeding of the Design Automation Conference, 656\u2013661.. ACM, Anaheim, USA."},{"key":"41_CR55","first-page":"401","volume-title":"21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, London, UK, April 2015. Lecture Notes in Computer Science, vol 9035","author":"D Beyer","year":"2015","unstructured":"Beyer D (2015) Software verification and verifiable witnesses\u2014(Report on SV-COMP 2015) In: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, London, UK, April 2015. Lecture Notes in Computer Science, vol 9035, 401\u2013416.. Springer, London, UK."},{"key":"41_CR56","first-page":"174","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, UK, March 2009. Lecture Notes in Computer Science, vol 5505","author":"R Brummayer","year":"2009","unstructured":"Brummayer R, Biere A (2009) Boolector: An efficient SMT solver for bit-vectors and arrays In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, UK, March 2009. Lecture Notes in Computer Science, vol 5505, 174\u2013177.. Springer, Heidelberg."},{"key":"41_CR57","first-page":"337","volume-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary, April 2008. Lecture Notes in Computer Science, vol 4963","author":"LM de Mouram","year":"2008","unstructured":"de Mouram LM, Bjorner N (2008) Z3: An efficient SMT solver In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary, April 2008. Lecture Notes in Computer Science, vol 4963, 337\u2013340.. Springer, Heidelberg."},{"issue":"4","key":"41_CR58","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 (1992) On computing the worst-case peak gain of linear systems. Syst Control Lett 19(4): 265\u2013269.","journal-title":"Syst Control Lett"},{"key":"41_CR59","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511781667","volume-title":"Digital signal processing: systems analysis and design","author":"PSR Diniz","year":"2010","unstructured":"Diniz PSR, da Silva EAB, Netto SL (2010) Digital signal processing: systems analysis and design. 2nd ed. Cambridge University Press, Cambridge, UK."},{"key":"41_CR60","unstructured":"Texas Instrument\u2122 (2013) MSP430G2231 Mixed signal controller. \n                    http:\/\/www.ti.com\/lit\/ds\/symlink\/msp430g2231-ep.pdf\n                    \n                  . Accessed 21 Nov 2013."},{"key":"41_CR61","unstructured":"GNU (2015) The GNU C reference manual. \n                    http:\/\/www.gnu.org\/software\/gnu-c-manual\/\n                    \n                  . Accessed 15 June 2015."},{"key":"41_CR62","volume-title":"Using a model checker to determine worst-case execution time. Technical Report","author":"S Kim","year":"2009","unstructured":"Kim S, Patel HD, Edwards SA (2009) Using a model checker to determine worst-case execution time. Technical Report. Computer Science Department, Columbia University."},{"key":"41_CR63","unstructured":"Texas Instrument\u2122 (2013) Code Composer Studio\u2122Integrated Development Environment for MSP430. \n                    http:\/\/www.ti.com\/tool\/ccstudio-msp430\n                    \n                  . Accessed 19 Nov 2013."},{"issue":"4","key":"41_CR64","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 (2007) Error analysis of digital filters using HOL theorem proving. J Appl Log 5(4): 651\u2013666.","journal-title":"J Appl Log"},{"key":"41_CR65","doi-asserted-by":"publisher","DOI":"10.1201\/9781439828632","volume-title":"MATLAB primer","author":"TA Davis","year":"2010","unstructured":"Davis TA (2010) MATLAB primer. 7th ed.. CRC Press, Washington, USA."},{"key":"41_CR66","first-page":"8043","volume-title":"IEEE International Conference on Acoustics, Speech and Signal Processing, Florence, Italy, May 2014. Proceedings of ICASSP 2014","author":"D Luengo","year":"2014","unstructured":"Luengo D, Oses D, Martino L (2014) Monte Carlo limit cycle characterization In: IEEE International Conference on Acoustics, Speech and Signal Processing, Florence, Italy, May 2014. Proceedings of ICASSP 2014, 8043\u20138047.. IEEE, Florence, Italy."},{"key":"41_CR67","first-page":"91","volume-title":"International Conference on Formal Methods in Computer-Aided Design, Austin, USA, October 2011. Proceedings of FMAC","author":"R K\u00f6nighofer","year":"2011","unstructured":"K\u00f6nighofer R, Bloem R (2011) Automated error localization and correction for imperative programs In: International Conference on Formal Methods in Computer-Aided Design, Austin, USA, October 2011. Proceedings of FMAC, 91\u2013100.. IEEE, Austin, USA."}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1186\/s13173-016-0041-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13173-016-0041-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13173-016-0041-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13173-016-0041-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,13]],"date-time":"2024-08-13T10:45:54Z","timestamp":1723545954000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1186\/s13173-016-0041-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,20]]},"references-count":67,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["41"],"URL":"https:\/\/doi.org\/10.1186\/s13173-016-0041-8","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"value":"0104-6500","type":"print"},{"value":"1678-4804","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,20]]},"assertion":[{"value":"22 October 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 May 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"1"}}