{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:57:17Z","timestamp":1743101837311,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030921231"},{"type":"electronic","value":"9783030921248"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-92124-8_25","type":"book-chapter","created":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T17:18:47Z","timestamp":1638465527000},"page":"443-460","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Bit-Precise Verification of\u00a0Discontinuity Errors Under 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-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":[[2021,12,3]]},"reference":[{"key":"25_CR1","unstructured":"MISRA-C:2004 \u2014 Guidelines for the use of the C language in critical systems. Technical report, MIRA Ltd. (2004)"},{"key":"25_CR2","unstructured":"Programming languages \u2014 C \u2014 Extensions to support embedded processors. ISO\/IEC Technical Report 18037:2008. EEE, New York (2008)"},{"key":"25_CR3","unstructured":"DO-178C\/ED-12C, Software considerations in airborne systems and equipment certification. Technical report, RTCA\/EUROCAE (2011)"},{"key":"25_CR4","unstructured":"ISO 26262 Road Vehicles - Functional Safety. Technical report. ISO, Geneva, Switzerland (2011)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-63387-9_23","volume-title":"Computer Aided Verification","author":"A Abate","year":"2017","unstructured":"Abate, A., et al.: Automated formal synthesis of digital controllers for state-space physical plants. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 462\u2013482. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_23"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Bessa, I., Abreu, R.B., Filho, J.E.C., Cordeiro, L.C.: SMT-based bounded model checking of fixed-point digital controllers. In: IECON, pp. 295\u2013301. IEEE (2014)","DOI":"10.1109\/IECON.2014.7048514"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD, pp. 69\u201376. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"issue":"8","key":"25_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/2240236.2240262","volume":"55","author":"S Chaudhuri","year":"2012","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM 55(8), 107\u2013115 (2012)","journal-title":"Commun. ACM"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: POPL, pp. 235\u2013248. ACM (2014)","DOI":"10.1145\/2578855.2535874"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Towards a compiler for reals. ACM Trans. Program. Lang. Syst. 39(2), 8:1\u20138:28 (2017)","DOI":"10.1145\/3014426"},{"key":"25_CR12","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":"25_CR13","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":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-63618-0_11","volume-title":"Software Verification","author":"MR Gadelha","year":"2020","unstructured":"Gadelha, M.R., Cordeiro, L.C., Nicole, D.A.: An efficient floating-point bit-blasting API for verifying C programs. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds.) NSV\/VSTTE -2020. LNCS, vol. 12549, pp. 178\u2013195. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63618-0_11"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-14295-6_22","volume-title":"Computer Aided Verification","author":"K Ghorbal","year":"2010","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212\u2013226. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_22"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-45237-7_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Giacobbe","year":"2020","unstructured":"Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: TACAS 2020. LNCS, vol. 12079, pp. 79\u201397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_5"},{"key":"25_CR17","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":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-03542-0_4","volume-title":"Programming Languages and Systems","author":"E Goubault","year":"2013","unstructured":"Goubault, E., Putot, S.: Robustness analysis of finite precision implementations. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 50\u201357. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_4"},{"key":"25_CR19","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":"25_CR20","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":"25_CR21","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":"25_CR22","unstructured":"Jet Propulsion Laboratory, C.I.o.T.: JPL Institutional Coding Standard for the C Programming Language. Standard (2009)"},{"key":"25_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":"25_CR24","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.sysarc.2016.11.010","volume":"76","author":"M Martel","year":"2017","unstructured":"Martel, M., Najahi, A., Revy, G.: Trade-offs of certified fixed-point code synthesis for linear algebra basic blocks. J. Syst. Archit. 76, 133\u2013148 (2017)","journal-title":"J. Syst. Archit."},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Martinez, A.A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT, pp. 9\u201318. ACM (2010)","DOI":"10.1145\/1879021.1879024"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: AAAI, pp. 6615\u20136624. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"25_CR27","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":"25_CR28","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. LNCS, vol. 10205, pp. 153\u2013169. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_9"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Salamati, M., Salvia, R., Darulova, E., Soudjani, S., Majumdar, R.: Memory-efficient mixed-precision implementations for robust explicit model predictive control. ACM Trans. Embed. Comput. Syst. 18(5s), 100:1\u2013100:19 (2019)","DOI":"10.1145\/3358223"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-030-63461-2_17","volume-title":"Integrated Formal Methods","author":"S Simi\u0107","year":"2020","unstructured":"Simi\u0107, S., Bemporad, A., Inverso, O., Tribastone, M.: Tight error analysis in fixed-point arithmetic. In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 318\u2013336. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_17"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Baranowski, M.S., Briggs, I., Jacobsen, C., Rakamari\u0107, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Trans. Program. Lang. Syst. 41(1), 2:1\u20132:39 (2019)","DOI":"10.1145\/3230733"},{"key":"25_CR32","unstructured":"Stol, J., De Figueiredo, L.H.: Self-validated numerical methods and applications. In: Monograph for 21st Brazilian Mathematics Colloquium, IMPA. Citeseer (1997)"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Tabuada, P., Balkan, A., Caliskan, S.Y., Shoukry, Y., Majumdar, R.: Input-output robustness for discrete systems. In: EMSOFT, pp. 217\u2013226. ACM (2012)","DOI":"10.1145\/2380356.2380396"},{"key":"25_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-319-73721-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Titolo","year":"2018","unstructured":"Titolo, L., Feli\u00fa, M.A., Moscato, M., Mu\u00f1oz, C.A.: An abstract interpretation framework for the round-off error analysis of floating-point programs. In: VMCAI 2018. LNCS, vol. 10747, pp. 516\u2013537. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_24"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-030-63461-2_8","volume-title":"Integrated Formal Methods","author":"L Titolo","year":"2020","unstructured":"Titolo, L., Moscato, M., Feliu, M.A., Mu\u00f1oz, C.A.: Automatic generation of guard-stable floating-point code. In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 141\u2013159. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_8"},{"key":"25_CR36","unstructured":"Yates, R.: Fixed-point arithmetic: an introduction. Digital Signal Labs (2009)"},{"key":"25_CR37","unstructured":"Zhao, Y., Shumailov, I., Mullins, R.D., Anderson, R.: To compress or not to compress: understanding the interactions between adversarial attacks and neural network compression. In: MLSys. mlsys.org (2019)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-92124-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T16:36:38Z","timestamp":1726245398000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-92124-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030921231","9783030921248"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-92124-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"3 December 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/","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":"86","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":"22","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":"4","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":"26% - 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)"}}]}}