{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:40:20Z","timestamp":1784328020564,"version":"3.55.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_3","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"21-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm"],"prefix":"10.1007","author":[{"given":"Mariano M.","family":"Moscato","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laura","family":"Titolo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco A.","family":"Feli\u00fa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"3_CR1","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language, version 1.12 (2016)"},{"issue":"2\u20133","key":"3_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J Bertrane","year":"2015","unstructured":"Bertrane, J., et al.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Prog. Lang. 2(2\u20133), 71\u2013190 (2015)","journal-title":"Found. Trends Prog. Lang."},{"issue":"6","key":"3_CR3","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17(6), 709\u2013727 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"3_CR4","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-012-9255-4","volume":"50","author":"S Boldo","year":"2013","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reasoning 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.C.: Formal verification of floating-point programs. In: Proceedings of ARITH18 2007, pp. 187\u2013194. IEEE Computer Society (2007)","DOI":"10.1109\/ARITH.2007.20"},{"issue":"4","key":"3_CR6","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s11786-011-0099-9","volume":"5","author":"S Boldo","year":"2011","unstructured":"Boldo, S., March\u00e9, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. Math. Comput. Sci. 5(4), 377\u2013393 (2011)","journal-title":"Math. Comput. Sci."},{"key":"3_CR7","unstructured":"Boldo, S., Mu\u00f1oz, C.: A high-level formalization of floating-point numbers in PVS. Technical Report CR-2006-214298, NASA (2006)"},{"key":"3_CR8","unstructured":"Bouissou, O., et al.: Space software validation using abstract interpretation. In: Proceedings of the International Space System Engineering Conference, Data Systems in Aerospace, DASIA 2009, pp. 1\u20137. ESA publications (2009)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","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.) APLAS 2008. LNCS, vol. 5356, pp. 3\u201318. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-89330-1_2"},{"issue":"2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2008.04.080","volume":"198","author":"S Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): semantic combination of congruence closure with solvable theories. Electron. Notes Theoret. Comput. Sci. 198(2), 51\u201369 (2008)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of tha 4th ACM Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR12","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Theorem Proving in Higher Order Logics","author":"M Daumas","year":"2001","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library for floating-point numbers and its application to exact computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 169\u2013184. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44755-5_13"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-540-74061-2_27","volume-title":"Static Analysis","author":"D Delmas","year":"2007","unstructured":"Delmas, D., Souyris, J.: Astr\u00e9e: from research to industry. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 437\u2013451. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74061-2_27"},{"issue":"2","key":"3_CR15","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)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15\u201329. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30482-1_10"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-38088-4_31","volume-title":"NASA Formal Methods","author":"AE Goodloe","year":"2013","unstructured":"Goodloe, A.E., Mu\u00f1oz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: from real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441\u2013446. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38088-4_31"},{"key":"3_CR18","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). \nhttps:\/\/doi.org\/10.1007\/11823230_3"},{"key":"3_CR19","unstructured":"IEEE: IEEE standard for binary floating-point arithmetic. Technical report, Institute of Electrical and Electronics Engineers (2008)"},{"issue":"3","key":"3_CR20","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)","journal-title":"Formal Aspects Comput."},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/j.scico.2014.04.003","volume":"96","author":"C March\u00e9","year":"2014","unstructured":"March\u00e9, C.: Verification of the functional behavior of a floating-point program: an industrial case study. Sci. Comput. Prog. 96, 279\u2013296 (2014)","journal-title":"Sci. Comput. Prog."},{"key":"3_CR22","unstructured":"March\u00e9, C., Moy, Y.: The Jessie Plugin for Deductive Verification in Frama-C (2017)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3\u201317. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24725-8_2"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-66266-4_14","volume-title":"Computer Safety, Reliability, and Security","author":"M Moscato","year":"2017","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.A.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 213\u2013229. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66266-4_14"},{"key":"3_CR25","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":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-54108-7_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Narkawicz","year":"2014","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 326\u2013343. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54108-7_17"},{"key":"3_CR27","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: The MINERVA software development process. In: 6th Workshop on Automated Formal Methods, AFM 2017 (2017)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Salvia, R., Titolo, L., Feli\u00fa, M., Moscato, M., Mu\u00f1oz, C.,Rakamaric, Z.: A mixed real and floating-point solver. In: 11th Annual NASAFormal Methods Symposium (NFM 2019) (2019)","DOI":"10.1007\/978-3-030-20652-9_25"},{"key":"3_CR30","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. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 516\u2013537. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73721-8_24"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-319-95582-7_22","volume-title":"Formal Methods","author":"L Titolo","year":"2018","unstructured":"Titolo, L., Moscato, M.M., Mu\u00f1oz, C.A., Dutle, A., Bobot, F.: A formally verified floating-point implementation of the compact position reporting algorithm. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 364\u2013381. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-95582-7_22"},{"key":"3_CR32","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). \nhttps:\/\/doi.org\/10.1007\/978-3-030-13838-7_10"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:05:58Z","timestamp":1588658758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","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":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","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":"129","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":"44","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":"7","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":"34% - 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":"4","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":"5,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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}