{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T22:55:59Z","timestamp":1771023359745,"version":"3.50.1"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle\/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_6","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:30Z","timestamp":1753089630000},"page":"122-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Formally Verified IEEE 754 Floating-Point Implementation of\u00a0Interval Iteration for\u00a0MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2908-8838","authenticated-orcid":false,"given":"Bram","family":"Kohlen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2612-2335","authenticated-orcid":false,"given":"Maximilian","family":"Sch\u00e4ffeler","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8244-518X","authenticated-orcid":false,"given":"Mohammad","family":"Abdulaziz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3576-0504","authenticated-orcid":false,"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point java programs in KeY. In: Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, pp. 242\u2013261 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_13","DOI":"10.1007\/978-3-030-72013-1_13"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - the KeY Book - from Theory to Practice (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Kellison, A.: Vcfloat2: Floating-point error analysis in Coq. In: CPP, pp. 14\u201329. ACM (2024)","DOI":"10.1145\/3636501.3636953"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C.: Probabilistic Model Checking. In: Dependable Software Systems Engineering, pp. 1\u201323. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-1","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model Checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"9","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and Model Checking join forces. Commun. ACM 9, 76\u201385 (2010). https:\/\/doi.org\/10.1145\/1810891.1810912","journal-title":"Commun. ACM"},{"key":"6_CR7","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov Decision Processes. In: 29th International Conference on Computer Aided Verification (CAV), pp. 160\u2013180 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: TYPES. pp. 34\u201350 (2003)","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"5","author":"G Barrett","year":"1989","unstructured":"Barrett, G.: Formal methods applied to a floating-point number system. IEEE Trans. Software Eng. 5, 611\u2013621 (1989). https:\/\/doi.org\/10.1109\/32.24710","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR11","first-page":"679","volume":"5","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 5, 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"10","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 10, 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Boldo, S., Melquiond, G.: FLOCQ: a unified library for proving floating-point algorithms in Coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243\u2013252 (2011). https:\/\/doi.org\/10.1109\/ARITH.2011.40","DOI":"10.1109\/ARITH.2011.40"},{"key":"6_CR14","unstructured":"Boldo, S., Munoz, C.: A high-level formalization of floating-point number in PVS. Tech. report (2006)"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 151\u2013168 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification (QComp 2020 competition report). In: 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA), pp. 216\u2013241 (2020). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pp. 21\u201330 (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV), pp. 39\u201356 (2001). https:\/\/doi.org\/10.1007\/3-540-44804-7_3","DOI":"10.1007\/3-540-44804-7_3"},{"key":"6_CR19","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, USA (1997)"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"2","author":"F De Dinechin","year":"2010","unstructured":"De Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using GAPPA. IEEE Trans. Comput. 2, 242\u2013253 (2010). https:\/\/doi.org\/10.1109\/TC.2010.128","journal-title":"IEEE Trans. Comput."},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, pp. 232\u2013247 (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: 8th International Workshop on Reachability Problems (RP), pp. 125\u2013137 (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Interval Iteration algorithm for MDPs and IMDPs. Theoretical Computer Science, pp. 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/J.TCS.2016.12.003","DOI":"10.1016\/J.TCS.2016.12.003"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"2","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 2, 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Formal verification at Intel. In: 18th Annual IEEE Symposium of Logic in Computer Science, 2003, pp. 45\u201354 (2003). https:\/\/doi.org\/10.1109\/LICS.2003.1210044","DOI":"10.1109\/LICS.2003.1210044"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Theorem Proving in Higher Order Logics, pp. 113\u2013130 (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_9","DOI":"10.1007\/3-540-48256-3_9"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: Correct probabilistic Model Checking with floating-point arithmetic. In: TACAS (2), pp. 41\u201359 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3","DOI":"10.1007\/978-3-030-99527-0_3"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 593\u2013598 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP Model Checking algorithms. In: 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 469\u2013488 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: 32nd International Conference on Computer Aided Verification (CAV), pp. 488\u2013511 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 344\u2013350 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kohlen, B., Lammich, P.: Fast verified SCCs for probabilistic Model Checking. In: ATVA (1), pp. 181\u2013202 (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_9","DOI":"10.1007\/978-3-031-45329-8_9"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kohlen, B., Lammich, P.: Efficient formally verified Maximal End Component decomposition for MDPs. In: FM (1), pp. 206\u2013225 (2024). https:\/\/doi.org\/10.1007\/978-981-99-8664-4","DOI":"10.1007\/978-981-99-8664-4"},{"key":"6_CR34","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/S10817-016-9401-5","volume":"3","author":"J H\u00f6lzl","year":"2017","unstructured":"H\u00f6lzl, J.: Markov chains and Markov decision processes in Isabelle\/HOL. J. Autom. Reason. 3, 345\u2013387 (2017). https:\/\/doi.org\/10.1007\/S10817-016-9401-5","journal-title":"J. Autom. Reason."},{"key":"6_CR35","unstructured":"H\u00f6lzl, J., Nipkow, T.: Markov models. Arch. Formal Proofs (2012)"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Kamali, M., Katoen, J.P.: Probabilistic model checking of AODV. In: 17th International Conference on the Quantitative Evaluation of Systems (QEST), pp. 54\u201373 (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_6","DOI":"10.1007\/978-3-030-59854-9_6"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Kellison, A.E., Appel, A.W., Tekriwal, M., Bindel, D.: LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs. In: ARITH, pp. 36\u201343. IEEE (2023)","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"6_CR38","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/S00165-014-0326-7","volume":"3","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 3, 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/S00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Kohlen, B., Sch\u00e4ffeler, M., Abdulaziz, M., Hartmanns, A., Lammich, P.: Artifact for the paper. In: A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. 4TU.ResearchData (2025). https:\/\/doi.org\/10.4121\/bf0fef24-4f0f-4de6-a58d-07b9ba601804","DOI":"10.4121\/bf0fef24-4f0f-4de6-a58d-07b9ba601804"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Kosmatov, N., Prevosto, V., Signoles, J.: Guide to software verification with Frama-C. Springer (2024)","DOI":"10.1007\/978-3-031-55608-1"},{"key":"6_CR41","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: 10th International Conference on Interactive Theorem Proving (ITP), pp. 22:1\u201322:19 (2019). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2019.22","DOI":"10.4230\/LIPICS.ITP.2019.22"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: 3rd International Conference on Interactive Theorem Proving (ITP), pp. 166\u2013182 (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12","DOI":"10.1007\/978-3-642-32347-8_12"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: CGO, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"Magron, V., Constantinides, G.A., Donaldson, A.F.: Certified roundoff error bounds using Semidefinite Programming. ACM Trans. Math. Softw. (4), 34:1\u201334:31 (2017). https:\/\/doi.org\/10.1145\/3015465","DOI":"10.1145\/3015465"},{"key":"6_CR45","unstructured":"Miner, P.S.: Defining the IEEE-854 floating-point standard in PVS. Technical report (1995)"},{"key":"6_CR46","doi-asserted-by":"publisher","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.A.: Automatic estimation of verified floating-point round-off errors via Static Analysis. In: Computer Safety, Reliability, and Security, pp. 213\u2013229 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_14","DOI":"10.1007\/978-3-319-66266-4_14"},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR48","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete stochastic Dynamic Programming. Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"6_CR49","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.P.: Sound value iteration. In: 30th International Conference on Computer Aided Verification (CAV), pp. 643\u2013661 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"6_CR50","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pp. 55\u201374 (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"6_CR51","doi-asserted-by":"publisher","unstructured":"Roberts, R., et al.: Probabilistic verification for reliability of a two-by-two network-on-chip system. In: 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS), pp. 232\u2013248 (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_16","DOI":"10.1007\/978-3-030-85248-1_16"},{"key":"6_CR52","doi-asserted-by":"publisher","unstructured":"Ruijters, E., Guck, D., Drolenga, P., Peters, M., Stoelinga, M.: Maintenance analysis and optimization via statistical Model Checking \u2013 evaluating a train pneumatic compressor. In: 13th International Conference on the Quantitative Evaluation of Systems (QEST), pp. 331\u2013347 (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_22","DOI":"10.1007\/978-3-319-43425-4_22"},{"key":"6_CR53","doi-asserted-by":"publisher","unstructured":"Ruijters, E., Guck, D., van Noort, M., Stoelinga, M.: Reliability-centered maintenance of the electrically insulated railway joint via fault tree analysis: a practical experience report. In: 46th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 662\u2013669 (2016). https:\/\/doi.org\/10.1109\/DSN.2016.67","DOI":"10.1109\/DSN.2016.67"},{"key":"6_CR54","doi-asserted-by":"publisher","unstructured":"Sch\u00e4ffeler, M., Abdulaziz, M.: Formally verified solution methods for infinite-horizon Markov Decision Processes. In: The 37th AAAI Conference on Artificial Intelligence (AAAI) (2023). https:\/\/doi.org\/10.1609\/aaai.v37i12.26759","DOI":"10.1609\/aaai.v37i12.26759"},{"key":"6_CR55","doi-asserted-by":"crossref","unstructured":"Sch\u00e4ffeler, M., Abdulaziz, M.: Formally verified approximate policy iteration. In: The 38th AAAI Conference on Artificial Intelligence (AAAI) (2025)","DOI":"10.1609\/aaai.v39i25.34868"},{"key":"6_CR56","doi-asserted-by":"publisher","unstructured":"Solovyev, A., Baranowski, M.S., Briggs, I., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Trans. Program. Lang. Syst. (1), 2:1\u20132:39 (2019). https:\/\/doi.org\/10.1145\/3230733","DOI":"10.1145\/3230733"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning \u2013 An Introduction. MIT Press (1998)","DOI":"10.1109\/TNN.1998.712192"},{"key":"6_CR58","doi-asserted-by":"publisher","unstructured":"Titolo, L., Moscato, M., Feliu, M.A., Masci, P., Mu\u00f1oz, C.A.: Rigorous Floating-Point Round-Off Error Analysis in\u00a0PRECiSA 4.0. In: Formal Methods, pp. 20\u201338 (2025). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_2","DOI":"10.1007\/978-3-031-71177-0_2"},{"key":"6_CR59","doi-asserted-by":"publisher","unstructured":"Vajjha, K., Shinnar, A., Trager, B.M., Pestun, V., Fulton, N.: CertRL: formalizing convergence proofs for value and policy iteration in CoQ. In: The 10th International Conference on Certified Programs and Proofs (CPP), pp. 18\u201331 (2021). https:\/\/doi.org\/10.1145\/3437992.3439927","DOI":"10.1145\/3437992.3439927"},{"key":"6_CR60","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989, London, UK, September 11\u201313, 1989, pp. 347\u2013359 (1989). https:\/\/doi.org\/10.1145\/99370.99404","DOI":"10.1145\/99370.99404"},{"key":"6_CR61","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., Becker, B.: Probabilistic model checking and reliability of results. In: 11th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pp. 207\u2013212 (2008). https:\/\/doi.org\/10.1109\/DDECS.2008.4538787","DOI":"10.1109\/DDECS.2008.4538787"},{"key":"6_CR62","unstructured":"Yu, L.: A formal model of IEEE floating point arithmetic. Arch. Formal Proofs (2013)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:35Z","timestamp":1753089635000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}