{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T17:12:21Z","timestamp":1789837941255,"version":"4.0.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T00:00:00Z","timestamp":1648684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003407","name":"MIUR","doi-asserted-by":"crossref","award":["PRIN 2017TWRCNB SEDUCE, and PRIN 2017FTXR7S IT-MATTERS"],"award-info":[{"award-number":["PRIN 2017TWRCNB SEDUCE, and PRIN 2017FTXR7S IT-MATTERS"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2022,3,31]]},"abstract":"<jats:p>We consider the problem of estimating the numerical accuracy of programs with operations in fixed-point arithmetic and variables of arbitrary, mixed precision, and possibly non-deterministic value. By applying a set of parameterised rewrite rules, we transform the relevant fragments of the program under consideration into sequences of operations in integer arithmetic over vectors of bits, thereby reducing the problem as to whether the error enclosures in the initial program can ever exceed a given order of magnitude to simple reachability queries on the transformed program. We describe a possible verification flow and a prototype analyser that implements our technique. We present an experimental evaluation on a particularly complex industrial case study, including a preliminary comparison between bit-level and word-level decision procedures.<\/jats:p>","DOI":"10.1145\/3524051","type":"journal-article","created":{"date-parts":[[2022,5,4]],"date-time":"2022-05-04T11:15:44Z","timestamp":1651662944000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Tight Error Analysis in Fixed-point Arithmetic"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5811-1091","authenticated-orcid":false,"given":"Stella","family":"Simi\u0107","sequence":"first","affiliation":[{"name":"IMT School for Advanced Studies, Lucca, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6761-0856","authenticated-orcid":false,"given":"Alberto","family":"Bemporad","sequence":"additional","affiliation":[{"name":"IMT School for Advanced Studies, Lucca, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-1979","authenticated-orcid":false,"given":"Omar","family":"Inverso","sequence":"additional","affiliation":[{"name":"Gran Sasso Science Institute, L\u2019Aquila, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6018-5989","authenticated-orcid":false,"given":"Mirco","family":"Tribastone","sequence":"additional","affiliation":[{"name":"IMT School for Advanced Studies, Lucca, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_1_2_2","article-title":"Verifying fixed-point digital filters using SMT-based bounded model checking","volume":"1305","author":"Abreu Renato B.","year":"2013","unstructured":"Renato B. Abreu, Lucas C. Cordeiro, and Eddie B. L. Filho. 2013. Verifying fixed-point digital filters using SMT-based bounded model checking. CoRR abs\/1305.2892 (2013).","journal-title":"CoRR"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-2256-8"},{"key":"e_1_3_1_4_2","first-page":"127","volume-title":"IJCAR (LNCS)","author":"Ayad Ali","year":"2010","unstructured":"Ali Ayad and Claude March\u00e9. 2010. Multi-prover verification of floating-point programs. In IJCAR (LNCS), Vol. 6173. Springer, 127\u2013141."},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u0107 Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In CAV. Springer-Verlag Berlin 171\u2013177.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9rome Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2003. A static analyzer for large safety-critical software. In PLDI. ACM SIGPLAN 196?207.","DOI":"10.1145\/780822.781153"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1561\/2200000016"},{"key":"e_1_3_1_8_2","volume-title":"TACAS (LNCS)","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT solver. In TACAS (LNCS), Vol. 7795. Springer."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2017.2696742"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.automatica.2018.10.050","article-title":"Complexity and convergence certification of a block principal pivoting method for box-constrained quadratic programs","volume":"100","author":"Cimini G.","year":"2019","unstructured":"G. Cimini and A. Bemporad. 2019. Complexity and convergence certification of a block principal pivoting method for box-constrained quadratic programs. Automatica 100 (2019), 29\u201337.","journal-title":"Automatica"},{"key":"e_1_3_1_11_2","first-page":"168","volume-title":"TACAS","author":"Clarke Edmund M.","year":"2004","unstructured":"Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In TACAS. 168\u2013176."},{"key":"e_1_3_1_12_2","volume-title":"POPL","author":"Darulova Eva","year":"2014","unstructured":"Eva Darulova and Viktor Kuncak. 2014. Sound compilation of reals. In POPL. ACM."},{"issue":"2","key":"e_1_3_1_13_2","article-title":"Towards a compiler for reals","volume":"39","author":"Darulova Eva","year":"2017","unstructured":"Eva Darulova and Viktor Kuncak. 2017. Towards a compiler for reals. ACM Trans. Program. Lang. Syst. 39, 2 (2017).","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_1_14_2","first-page":"22:1\u201322:10","volume-title":"EMSOFT","author":"Darulova Eva","year":"2013","unstructured":"Eva Darulova, Viktor Kuncak, Rupak Majumdar, and Indranil Saha. 2013. Synthesis of fixed-point programs. In EMSOFT. IEEE, 22:1\u201322:10."},{"key":"e_1_3_1_15_2","first-page":"49","volume-title":"SBESC","author":"Bessa Iury Valente de","year":"2014","unstructured":"Iury Valente de Bessa, Hussama Ibrahim Ismail, Lucas Carvalho Cordeiro, and Joao Edgar Chaves Filho. 2014. Verification of delta form realization in fixed-point digital controllers using bounded model checking. In SBESC. IEEE, 49\u201354."},{"key":"e_1_3_1_16_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo de","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin."},{"key":"e_1_3_1_17_2","first-page":"53","volume-title":"FMICS (LNCS)","author":"Delmas David","year":"2009","unstructured":"David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal, and Franck V\u00e9drine. 2009. Towards an industrial use of FLUCTUAT on safety-critical avionics software. In FMICS (LNCS), Vol. 5825. Springer, 53\u201369."},{"key":"e_1_3_1_18_2","first-page":"737","volume-title":"CAV","author":"Dutertre Bruno","year":"2014","unstructured":"Bruno Dutertre. 2014. Yices 2.2. In CAV(LNCS), Vol. 8559. Springer, 737\u2013744."},{"key":"e_1_3_1_19_2","first-page":"502","volume-title":"SAT (LNCS)","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. 2003. An extensible SAT-solver. In SAT (LNCS), Vol. 2919. Springer, 502\u2013518."},{"key":"e_1_3_1_20_2","first-page":"275","volume-title":"ICCAD","author":"Fang Claire Fang","year":"2003","unstructured":"Claire Fang Fang, Rob A. Rutenbar, and Tsuhan Chen. 2003. Fast, accurate static analysis for fixed-point finite-precision effects in DSP designs. In ICCAD. IEEE\/ACM, 275\u2013282."},{"key":"e_1_3_1_21_2","first-page":"710","volume-title":"ASE","author":"Fischer Bernd","year":"2013","unstructured":"Bernd Fischer, Omar Inverso, and Gennaro Parlato. 2013. CSeq: A concurrency pre-processor for sequential C verification tools. In ASE. IEEE, 710\u2013713."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240481"},{"key":"e_1_3_1_23_2","first-page":"211","volume-title":"SFM (LNCS)","author":"Harrison John","year":"2006","unstructured":"John Harrison. 2006. Floating-point verification using theorem proving. In SFM (LNCS), Vol. 3965. Springer, 211\u2013242."},{"key":"e_1_3_1_24_2","unstructured":"International Organization for Standardization. 2018. ISO-26262 Road vehicles \u2014 Functional safety. https:\/\/yurichev.com\/mirrors\/C\/JPL_Coding_Standard_C.pdf."},{"key":"e_1_3_1_25_2","first-page":"1","volume-title":"ICCPS","author":"Inverso Omar","year":"2018","unstructured":"Omar Inverso, Alberto Bemporad, and Mirco Tribastone. 2018. SAT-based synthesis of spoofing attacks in cyber-physical control systems. In ICCPS. IEEE\/ACM, 1\u20139."},{"key":"e_1_3_1_26_2","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1145\/3332466.3374529","volume-title":"PPoPP","author":"Inverso Omar","year":"2020","unstructured":"Omar Inverso and Catia Trubiani. 2020. Parallel and distributed bounded model checking of multi-threaded programs. In PPoPP. ACM, 202\u2013216."},{"key":"e_1_3_1_27_2","volume-title":"Information Technology\u2014Programming languages\u2014C","author":"SC22 ISO\/IEC JTC1","year":"2018","unstructured":"ISO\/IEC JTC1 SC22. 2018. Information Technology\u2014Programming languages\u2014C. Technical Report. International Organization for Standardization\/International Electrotechnical Commission."},{"key":"e_1_3_1_28_2","volume-title":"Information Technology\u2014Programming languages\u2014C\u2014Extensions to Support Embedded Processors","author":"WG14 ISO\/IEC JTC1 SC22","year":"2008","unstructured":"ISO\/IEC JTC1 SC22 WG14. 2008. Information Technology\u2014Programming languages\u2014C\u2014Extensions to Support Embedded Processors. Technical Report. International Organization for Standardization\/International Electrotechnical Commission."},{"key":"e_1_3_1_29_2","first-page":"49","volume-title":"MEMOCODE","author":"Ivancic Franjo","year":"2010","unstructured":"Franjo Ivancic, Malay K. Ganai, Sriram Sankaranarayanan, and Aarti Gupta. 2010. Numerical stability analysis of floating-point computations using software model checking. In MEMOCODE. IEEE, 49\u201358."},{"key":"e_1_3_1_30_2","unstructured":"California Institute of Technology Jet Propulsion Laboratory. 2009. JPL Institutional Coding Standard for the C Programming Language."},{"key":"e_1_3_1_31_2","first-page":"2849","volume-title":"ICML (JMLR Workshop and Conference Proceedings)","volume":"48","author":"Lin Darryl Dexu","year":"2016","unstructured":"Darryl Dexu Lin, Sachin S. Talathi, and V. Sreekanth Annapureddy. 2016. Fixed point quantization of deep convolutional networks. In ICML (JMLR Workshop and Conference Proceedings), Vol. 48. JMLR.org, 2849\u20132858."},{"key":"e_1_3_1_32_2","first-page":"322","volume-title":"IFM (LNCS)","author":"Lohar Debasmita","year":"2019","unstructured":"Debasmita Lohar, Milos Prokop, and Eva Darulova. 2019. Sound probabilistic numerical error analysis. In IFM (LNCS), Vol. 11918. Springer, 322\u2013340."},{"key":"e_1_3_1_33_2","first-page":"1","volume-title":"DASIP","author":"Martel Matthieu","year":"2014","unstructured":"Matthieu Martel, Amine Najahi, and Guillaume Revy. 2014. Toward the synthesis of fixed-point code for matrix inversion based on Cholesky decomposition. In DASIP. IEEE, 1\u20138."},{"key":"e_1_3_1_34_2","first-page":"9","volume-title":"EMSOFT","author":"Martinez Adolfo Anta","year":"2010","unstructured":"Adolfo Anta Martinez, Rupak Majumdar, Indranil Saha, and Paulo Tabuada. 2010. Automatic verification of control system implementations. In EMSOFT. ACM, 9\u201318."},{"key":"e_1_3_1_35_2","unstructured":"MIRA Ltd. 2004. MISRA-C:2004 Guidelines for the use of the C language in Critical Systems."},{"key":"e_1_3_1_36_2","volume-title":"On the Arithmetic Precision for Implementing Back-Propagation Networks on FPGA: A Case Study","author":"Moussa Medhat","year":"2006","unstructured":"Medhat Moussa, Shawki Areibi, and Kristian Nichols. 2006. On the Arithmetic Precision for Implementing Back-Propagation Networks on FPGA: A Case Study. Springer US."},{"key":"e_1_3_1_37_2","volume-title":"Synthesis of Certified Programs in Fixed-Point Arithmetic, and Its Application to Linear Algebra Basic Blocks","author":"Najahi Amine","year":"2014","unstructured":"Amine Najahi. 2014. Synthesis of Certified Programs in Fixed-Point Arithmetic, and Its Application to Linear Algebra Basic Blocks. Ph.D. Dissertation. Institution is Universit\u00e9 de Perpignan Via Domitia."},{"key":"e_1_3_1_38_2","first-page":"115","volume-title":"APLAS (LNCS)","author":"Navas Jorge A.","year":"2012","unstructured":"Jorge A. Navas, Peter Schachte, Harald S\u00f8ndergaard, and Peter J. Stuckey. 2012. Signedness-agnostic program analysis: Precise integer bounds for low-level code. In APLAS (LNCS), Vol. 7705. Springer, 115\u2013130."},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190101"},{"key":"e_1_3_1_40_2","first-page":"217","volume-title":"EMSOFT","author":"Pajic Miroslav","year":"2015","unstructured":"Miroslav Pajic, Junkil Park, Insup Lee, George J. Pappas, and Oleg Sokolsky. 2015. Automatic verification of linear controller software. In EMSOFT. IEEE, 217\u2013226."},{"key":"e_1_3_1_41_2","volume-title":"Computer Arithmetic: Algorithms and Hardware Designs","author":"Parhami Behrooz","year":"1999","unstructured":"Behrooz Parhami. 1999. Computer Arithmetic: Algorithms and Hardware Designs. Oxford University Press, Inc."},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2015.03.002"},{"key":"e_1_3_1_43_2","first-page":"318","volume-title":"IFM (Lecture Notes in Computer Science)","author":"Simic Stella","year":"2020","unstructured":"Stella Simic, Alberto Bemporad, Omar Inverso, and Mirco Tribastone. 2020. Tight error analysis in fixed-point arithmetic. In IFM (Lecture Notes in Computer Science), Vol. 12546. Springer, 318\u2013336."},{"key":"e_1_3_1_44_2","volume-title":"SEFM","author":"Simic Stella","year":"2021","unstructured":"Stella Simic, Omar Inverso, and Mirco Tribastone. 2021. Bit-precise verification of discontinuity errors under fixed-point arithmetic. In SEFM. Springer, 443\u2013460."},{"key":"e_1_3_1_45_2","volume-title":"Using the GNU Compiler Collection: A GNU Manual for GCC Version 4.3.3","author":"Stallman Richard M.","year":"2009","unstructured":"Richard M. Stallman and GCC DeveloperCommunity. 2009. Using the GNU Compiler Collection: A GNU Manual for GCC Version 4.3.3. CreateSpace, Scotts Valley, CA."},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","DOI":"10.1007\/s12532-020-00179-2","article-title":"OSQP: An operator splitting solver for quadratic programs","author":"Stellato B.","year":"2020","unstructured":"B. Stellato, G. Banjac, P. Goulart, A. Bemporad, and S. Boyd. 2020. OSQP: An operator splitting solver for quadratic programs. Math. Program. Computat. (2020). Retrieved from http:\/\/arxiv.org\/abs\/1711.08013.","journal-title":"Math. Program. Computat."},{"key":"e_1_3_1_47_2","volume-title":"Monograph for 21st Brazilian Mathematics Colloquium, IMPA","author":"Stol Jorge","year":"1997","unstructured":"Jorge Stol and Luiz Henrique De Figueiredo. 1997. Self-validated numerical methods and applications. In Monograph for 21st Brazilian Mathematics Colloquium, IMPA. Citeseer."},{"key":"e_1_3_1_48_2","first-page":"516","volume-title":"VMCAI (LNCS)","author":"Titolo Laura","year":"2018","unstructured":"Laura Titolo, Marco A. Feli\u00fa, Mariano M. Moscato, and C\u00e9sar A. Mu\u00f1oz. 2018. An abstract interpretation framework for the round-off error analysis of floating-point programs. In VMCAI (LNCS), Vol. 10747. Springer, 516\u2013537."},{"key":"e_1_3_1_49_2","article-title":"Fixed-point arithmetic: An introduction","author":"Yates Randy","year":"2009","unstructured":"Randy Yates. 2009. Fixed-point arithmetic: An introduction. Digit. Sig. Labs (2009).","journal-title":"Digit. Sig. Labs"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524051","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:37Z","timestamp":1750188637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,31]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,3,31]]}},"alternative-id":["10.1145\/3524051"],"URL":"https:\/\/doi.org\/10.1145\/3524051","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,31]]},"assertion":[{"value":"2021-06-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-02","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}