{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:14:24Z","timestamp":1742926464235,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030634605"},{"type":"electronic","value":"9783030634612"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-63461-2_17","type":"book-chapter","created":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T16:03:28Z","timestamp":1605283408000},"page":"318-336","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Tight Error Analysis in Fixed-Point Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5811-1091","authenticated-orcid":false,"given":"Stella","family":"Simi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6761-0856","authenticated-orcid":false,"given":"Alberto","family":"Bemporad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-1979","authenticated-orcid":false,"given":"Omar","family":"Inverso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6018-5989","authenticated-orcid":false,"given":"Mirco","family":"Tribastone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"17_CR1","unstructured":"Programming languages \u2013 C - Extensions to support embedded processors. EEE, New York (1987). iSO\/IEC Technical Report 18037:2008(E)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abreu, R.B., Cordeiro, L.C., Filho, E.B.L.: Verifying fixed-point digital filters using SMT-based bounded model checking. CoRR abs\/1305.2892 (2013)","DOI":"10.14209\/sbrt.2013.178"},{"issue":"1\u20132","key":"17_CR3","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\u20132), 173\u2013200 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-14203-1_11","volume-title":"Automated Reasoning","author":"A Ayad","year":"2010","unstructured":"Ayad, A., March\u00e9, C.: Multi-prover verification of floating-point programs. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 127\u2013141. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_11"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"de Bessa, I.V., Ismail, H.I., Cordeiro, L.C., Filho, J.E.C.: Verification of delta form realization in fixed-point digital controllers using bounded model checking. In: SBESC, pp. 49\u201354. IEEE (2014)","DOI":"10.1109\/SBESC.2014.14"},{"key":"17_CR6","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. CoRR (2007)"},{"issue":"1","key":"17_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2200000016","volume":"3","author":"S Boyd","year":"2011","unstructured":"Boyd, S., Parikh, N., Chu, E., Peleato, B., Eckstein, J.: Distributed optimization and statistical learning via the alternating direction method of multipliers. Found. Trends Mach. Learn. 3(1), 1\u2013122 (2011)","journal-title":"Found. Trends Mach. Learn."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Cimini, G., Bemporad, A.: Exact complexity certification of active-set methods for quadratic programming 62(12), 6094\u20136109 (2017)","DOI":"10.1109\/TAC.2017.2696742"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.automatica.2018.10.050","volume":"100","author":"G Cimini","year":"2019","unstructured":"Cimini, G., Bemporad, A.: Complexity and convergence certification of a block principal pivoting method for box-constrained quadratic programs. Automatica 100, 29\u201337 (2019)","journal-title":"Automatica"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: POPL, ACM (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V., Majumdar, R., Saha, I.: Synthesis of fixed-point programs. In: EMSOFT, pp. 22:1\u201322:10. IEEE (2013)","DOI":"10.1109\/EMSOFT.2013.6658600"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Fang, C.F., Rutenbar, R.A., Chen, T.: Fast, accurate static analysis for fixed-point finite-precision effects in DSP designs. In: ICCAD, pp. 275\u2013282. IEEE\/ACM (2003)","DOI":"10.1109\/ICCAD.2003.159701"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Fischer, B., Inverso, O., Parlato, G.: CSEQ: a concurrency pre-processor for sequential C verification tools. In: ASE, pp. 710\u2013713. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693139"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-18275-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Goubault","year":"2011","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232\u2013247. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11757283_8","volume-title":"Formal Methods for Hardware Verification","author":"J Harrison","year":"2006","unstructured":"Harrison, J.: Floating-point verification using theorem proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 211\u2013242. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11757283_8"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Inverso, O., Bemporad, A., Tribastone, M.: Sat-based synthesis of spoofing attacks in cyber-physical control systems. In: ICCPS, pp. 1\u20139. IEEE\/ACM (2018)","DOI":"10.1109\/ICCPS.2018.00009"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: PPoPP, pp. 202\u2013216. ACM (2020)","DOI":"10.1145\/3332466.3374529"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Ganai, M.K., Sankaranarayanan, S., Gupta, A.: Numerical stability analysis of floating-point computations using software model checking. In: MEMOCODE, pp. 49\u201358. IEEE (2010)","DOI":"10.1109\/MEMCOD.2010.5558622"},{"key":"17_CR21","unstructured":"Lin, D.D., Talathi, S.S., Annapureddy, V.S.: Fixed point quantization of deep convolutional networks. In: ICML. JMLR Workshop and Conference Proceedings, vol. 48, pp. 2849\u20132858. JMLR.org (2016)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-030-34968-4_18","volume-title":"Integrated Formal Methods","author":"D Lohar","year":"2019","unstructured":"Lohar, D., Prokop, M., Darulova, E.: Sound probabilistic numerical error analysis. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 322\u2013340. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_18"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Martel, M., Najahi, A., Revy, G.: Toward the synthesis of fixed-point code for matrix inversion based on cholesky decomposition. In: DASIP, pp. 1\u20138. IEEE (2014)","DOI":"10.1109\/DASIP.2014.7115609"},{"key":"17_CR24","unstructured":"Martinez, A.A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT, pp. 9\u201318. ACM (2010)"},{"key":"17_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-28487-7_2","volume-title":"FPGA Implementations of Neural Networks","author":"M Moussa","year":"2006","unstructured":"Moussa, M., Areibi, S., Nichols, K.: On the arithmetic precision for implementing back-propagation networks on FPGA: a case study. In: Omondi, A.R., Rajapakse, J.C. (eds.) FPGA Implementations of Neural Networks. Springer, Boston (2006). https:\/\/doi.org\/10.1007\/0-387-28487-7_2"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-35182-2_9","volume-title":"Programming Languages and Systems","author":"JA Navas","year":"2012","unstructured":"Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Signedness-agnostic program analysis: precise integer bounds for low-level code. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 115\u2013130. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_9"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Pajic, M., Park, J., Lee, I., Pappas, G.J., Sokolsky, O.: Automatic verification of linear controller software. In: EMSOFT. pp. 217\u2013226. IEEE (2015)","DOI":"10.1109\/EMSOFT.2015.7318277"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Patrinos, P., Guiggiani, A., Bemporad, A.: A dual gradient-projection algorithm for model predictive control in fixed-point arithmetic. Automatica (2015)","DOI":"10.1016\/j.automatica.2015.03.002"},{"key":"17_CR29","unstructured":"Stellato, B., Banjac, G., Goulart, P., Bemporad, A., Boyd, S.: OSQP: an operator splitting solver for quadratic programs. Mathematical Programming Computation (2020). http:\/\/arxiv.org\/abs\/1711.08013"},{"key":"17_CR30","unstructured":"Stol, J., De Figueiredo, L.H.: Self-validated numerical methods and applications. In: Monograph for 21st Brazilian Mathematics Colloquium, IMPA. Citeseer (1997)"},{"key":"17_CR31","unstructured":"Yates, R.: Fixed-point arithmetic: an introduction. Digital Signal Labs (2009)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63461-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T16:37:18Z","timestamp":1605285438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-63461-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030634605","9783030634612"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63461-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lugano","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm20.si.usi.ch\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic this event was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}