{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:33Z","timestamp":1775873493088,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"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><jats:p>Small round-off errors in safety-critical systems can lead to catastrophic consequences. In this context, determining if the result computed by a floating-point program is accurate enough with respect to its ideal real-number counterpart is essential. This paper presents PRECiSA 4.0, a tool that rigorously estimates the accumulated round-off error of a floating-point program. PRECiSA 4.0 combines static analysis, optimization techniques, and theorem proving to provide a modular approach for computing a provably correct round-off error estimation. PRECiSA 4.0 adds several features to previous versions of the tool that enhance its applicability and performance. These features include support for data collections such as lists, records, and tuples; support for recursion schemas; an updated floating-point formalization that closely characterizes the IEEE-754 standard; an efficient and modular analysis of function calls that improves the performances for large programs; and a new user interface integrated into Visual Studio Code.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_2","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"20-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Rigorous Floating-Point Round-Off Error Analysis in\u00a0PRECiSA 4.0"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7820-7640","authenticated-orcid":false,"given":"Laura","family":"Titolo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6468-9498","authenticated-orcid":false,"given":"Mariano","family":"Moscato","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6943-9479","authenticated-orcid":false,"given":"Marco A.","family":"Feliu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0667-7763","authenticated-orcid":false,"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8503-5514","authenticated-orcid":false,"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Abbasi, R., Darulova, E.: Modular optimization-based roundoff error analysis of floating-point programs. In: 30th International Symposium on Static Analysis, SAS 2023. LNCS, vol. 14284, pp. 41\u201364. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_4","DOI":"10.1007\/978-3-031-44245-2_4"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Adj\u00e9, A., Ben Khalifa, D., Martel, M.: Fast and efficient bit-level precision tuning. In: Proceedings of the 28th International Symposium on Static Analysis, SAS 2021. LNCS, vol. 12913, pp. 1\u201324. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_1","DOI":"10.1007\/978-3-030-88806-0_1"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Kellison, A.: VCFloat2: floating-point error analysis in Coq. In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pp. 14\u201329. ACM (2024). https:\/\/doi.org\/10.1145\/3636501.3636953","DOI":"10.1145\/3636501.3636953"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Becker, H., Zyuzin, N., Monat, R., Darulova, E., Myreen, M.O., Fox, A.C.J.: A verified certificate checker for finite-precision error bounds in Coq and HOL4. In: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603019","DOI":"10.23919\/FMCAD.2018.8603019"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Bernardes Fernandes\u00a0Ferreira, N., Moscato, M.M., Titolo, L., Ayala-Rinc\u00f3n, M.: A provably correct floating-point implementation of well clear avionics concepts. In: Formal Methods in Computer-Aided Design (FMCAD 2023), pp. 237\u2013246. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_32","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_32"},{"key":"2_CR6","unstructured":"Boldo, S., Mu\u00f1oz, C.: A high-level formalization of floating-point numbers in PVS, CR-2006-214298, NASA. Technical report (2006)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-89330-1_2","volume-title":"Programming Languages and Systems","author":"L Chen","year":"2008","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) Programming Languages and Systems, pp. 3\u201318. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89330-1_2"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Cherubin, S., Agosta, G.: Tools for reduced precision computation: a survey. ACM Comput. Surv. 53(2), 33:1\u201333:35 (2020). https:\/\/doi.org\/10.1145\/3381039","DOI":"10.1145\/3381039"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Chiang, W., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamari\u0107, Z.: Rigorous floating-point mixed-precision tuning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 300\u2013315. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009846","DOI":"10.1145\/3009837.3009846"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Damouche, N., Martel, M.: Salsa: an automatic tool to improve the numerical accuracy of programs. In: 6th Workshop on Automated Formal Methods, AFM 2017, vol. 5, pp. 63\u201376 (2017). https:\/\/doi.org\/10.29007\/j2fd","DOI":"10.29007\/j2fd"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Damouche, N., Martel, M., Panchekha, P., Qiu, C., Sanchez-Stern, A., Tatlock, Z.: Toward a standard benchmark format and suite for floating-point analysis. In: 9th International Workshop Numerical Software Verification, NSV 2016. LNCS, vol. 10152, pp. 63\u201377 (2016). https:\/\/doi.org\/10.1007\/978-3-319-54292-8_6","DOI":"10.1007\/978-3-319-54292-8_6"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-89960-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Darulova","year":"2018","unstructured":"Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy - framework for analysis and optimization of numerical programs (tool paper). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 270\u2013287. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_15"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 235\u2013248. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535874","DOI":"10.1145\/2535838.2535874"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Das, A., Briggs, I., Gopalakrishnan, G., Krishnamoorthy, S.: An abstraction-guided approach to scalable and rigorous floating-point error analysis. arXiv preprint arXiv:2004.11960 (2020)","DOI":"10.1109\/SC41405.2020.00055"},{"issue":"2","key":"2_CR16","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F de Dinechin","year":"2011","unstructured":"de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242\u2013253 (2011). https:\/\/doi.org\/10.1109\/TC.2010.128","journal-title":"IEEE Trans. Comput."},{"issue":"1\u20134","key":"2_CR17","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/B:NUMA.0000049462.70970.b6","volume":"37","author":"LH de Figueiredo","year":"2004","unstructured":"de Figueiredo, L.H., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1\u20134), 147\u2013158 (2004). https:\/\/doi.org\/10.1023\/B:NUMA.0000049462.70970.b6","journal-title":"Numer. Algorithms"},{"key":"2_CR18","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":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"E Goubault","year":"2006","unstructured":"Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18\u201334. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_3"},{"key":"2_CR20","unstructured":"Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis. arXiv preprint arxiv:0807.2961 (2008)"},{"key":"2_CR21","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":"2_CR22","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":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"2_CR24","unstructured":"IEEE: IEEE standard for binary floating-point arithmetic, Technical report, Institute of Electrical and Electronics Engineers (2008)"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Isychev, A., Darulova, E.: Scaling up roundoff analysis of functional data structure programs. In: Proceedings of the 30th International Symposium on Static Analysis, SAS 2023. LNCS, vol. 14284, pp. 371\u2013402. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_17","DOI":"10.1007\/978-3-031-44245-2_17"},{"issue":"3","key":"2_CR26","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/S00165-014-0326-7","volume":"27","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. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/S00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Proceedings of the 13th European Symposium on Programming Languages and Systems, ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_2","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Proceedings of the 36th International Conference on Computer Safety, Reliablilty, and Security, SAFECOMP 2017. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_14","DOI":"10.1007\/978-3-319-66266-4_14"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Moscato, M., Titolo, L., Feli\u00fa, M., Mu\u00f1oz, C.: Provably correct floating-point implementation of a point-in-polygon algorithm. In: Proceedings of the 23nd International Symposium on Formal Methods, FM 2019. LNCS, vol. 11800, pp. 21\u201337. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_3","DOI":"10.1007\/978-3-030-30942-8_3"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M.: DAIDALUS: detect and avoid alerting logic for unmanned systems. In: Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic (2015)","DOI":"10.1109\/DASC.2015.7311421"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Hagen, G.: Algorithms for collision detection between a point and a moving polygon, with applications to aircraft weather avoidance. In: Proceedings of the AIAA Aviation Conference (2016)","DOI":"10.2514\/6.2016-3598"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Proceedings of the 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013. LNCS, vol.\u00a08164, pp. 326\u2013343. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_17","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Proceedings of the 11th International Conference on Automated Deduction, CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 1\u201311. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737959","DOI":"10.1145\/2737924.2737959"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Ramananandro, T., Mountcastle, P., Meister, B., Lethin, R.: A unified Coq framework for verifying C programs with floating-point computations. In: Proceedings of CPP 2016, pp. 15\u201326. ACM (2016). https:\/\/doi.org\/10.1145\/2854065.2854066","DOI":"10.1145\/2854065.2854066"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Rubio-Gonz\u00e1lez, C., et al.: Precimonious: tuning assistant for floating-point precision. In: International Conference for High Performance Computing, Networking, Storage and Analysis, SC\u201913, pp. 27:1\u201327:12. ACM (2013). https:\/\/doi.org\/10.1145\/2503210.2503296","DOI":"10.1145\/2503210.2503296"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Solovyev, A., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. In: Proceedings of the 20th International Symposium on Formal Methods, FM 2015. LNCS, vol.\u00a09109, pp. 532\u2013550. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_33","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Th\u00e9venoux, L., Langlois, P., Martel, M.: Automatic source-to-source error compensation of floating-point programs. In: 18th IEEE International Conference on Computational Science and Engineering, CSE 2015, pp. 9\u201316. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/CSE.2015.11","DOI":"10.1109\/CSE.2015.11"},{"key":"2_CR39","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":"2_CR40","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":"2_CR41","doi-asserted-by":"publisher","unstructured":"Titolo, L., Moscato, M., Mu\u00f1oz, C., Dutle, A., Bobot, F.: A formally verified floating-point implementation of the compact position reporting algorithm. In: Proceedings of the 22nd International Symposium on Formal Methods, FM 2018. LNCS, vol. 10951, pp. 364\u2013381. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_22","DOI":"10.1007\/978-3-319-95582-7_22"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-030-13838-7_10","volume-title":"Logic-Based Program Synthesis and Transformation","author":"L Titolo","year":"2019","unstructured":"Titolo, L., Mu\u00f1oz, C.A., Feli\u00fa, M.A., Moscato, M.M.: Eliminating unstable tests in floating-point programs. In: Mesnard, F., Stuckey, P.J. (eds.) LOPSTR 2018. LNCS, vol. 11408, pp. 169\u2013183. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-13838-7_10"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Yi, X., Chen, L., Mao, X., Ji, T.: Efficient automated repair of high floating-point errors in numerical libraries. Proc. ACM Program. Lang. 3(POPL), 56:1\u201356:29 (2019). https:\/\/doi.org\/10.1145\/3290369","DOI":"10.1145\/3290369"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:11:10Z","timestamp":1726121470000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}