{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:41:03Z","timestamp":1764402063673,"version":"3.46.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"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,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>Recent advances in satisfiability modulo theories have brought practical software verification within reach. The advent of the LLVM project presents a common representation which allows verification between programs written in different languages such as C and Rust. New programming languages such as Rust often have less complete standard libraries. In this work, we explore using the SMACK software verifier to check the equivalence of math library routines from the  libm library and their translations into native Rust programs.<\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_12","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:22:12Z","timestamp":1746177732000},"page":"239-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Equivalence Checking of a libm Port"],"prefix":"10.1007","author":[{"given":"Mark\u00a0S.","family":"Baranowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Baranowski, M., He, S., Rakamaric, Z.: Verifying rust programs with smack. In: Lahiri, S.K., Wang, C. (eds.) Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 11138, pp. 528\u2013535. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_32","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24, https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Components and Objects (FMCO). pp. 364\u2013387 (200). https:\/\/doi.org\/10.1007\/11804192_17, https:\/\/link.springer.com\/chapter\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Kasampalis, T., Park, D., Lin, Z., Adve, V.S., Ro\u015fu, G.: Language-parametric compiler validation with application to llvm. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. p. 1004-1019. ASPLOS \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3445814.3446751, https:\/\/doi.org\/10.1145\/3445814.3446751","DOI":"10.1145\/3445814.3446751"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Hawblitzel, C., Kawaguchi, M., Rebelo, H.: Symdiff: A language-agnostic semantic diff tool for imperative programs. In: Computer Aided Verification (CAV \u201912) (Tool description). Springer (July 2012), https:\/\/www.microsoft.com\/en-us\/research\/publication\/symdiff-a-language-agnostic-semantic-diff-tool-for-imperative-programs\/","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: International Conference on Computer Aided Verification (CAV). pp. 427\u2013443 (2012)","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"12_CR8","unstructured":"Rust libm. https:\/\/crates.io\/crates\/libm"},{"key":"12_CR9","unstructured":"crates.io Rust libm dependents. https:\/\/crates.io\/crates\/libm\/reverse_dependencies"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Mal\u00edk, V., Vojnar, T.: Automatically checking semantic equivalence between versions of large-scale c projects. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). pp. 329\u2013339 (2021). https:\/\/doi.org\/10.1109\/ICST49551.2021.00045","DOI":"10.1109\/ICST49551.2021.00045"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Matsakis, N.D., Klock, II, F.S.: The Rust language. In: ACM SIGAda Annual Conference on High Integrity Language Technology (HILT). pp. 103\u2013104 (2014). https:\/\/doi.org\/10.1145\/2663171.2663188, http:\/\/doi.acm.org\/10.1145\/2663171.2663188","DOI":"10.1145\/2663171.2663188"},{"key":"12_CR12","unstructured":"musl libc. https:\/\/www.musl-libc.org"},{"key":"12_CR13","unstructured":"IEEE nextafter. https:\/\/en.cppreference.com\/w\/cpp\/numeric\/math\/nextafter"},{"key":"12_CR14","unstructured":"Incorrect exponent calculation in the nextafter implementations leads to missed overflow\/underflow signals $$\\cdot $$ issue #286. https:\/\/github.com\/rust-lang\/libm\/issues\/286"},{"key":"12_CR15","unstructured":"This updates the exponent calculations done in the nextafter functions to match their musl counterparts by keram88 $$\\cdot $$ pull request #287. https:\/\/github.com\/rust-lang\/libm\/pull\/287"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. pp. 669\u2013685. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_55"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Ro\u0219u, G., \u0218erb\u0103nut\u0103, T.F.: An overview of the k semantic framework. The Journal of Logic and Algebraic Programming 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1567832610000160, membrane computing and programming","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"12_CR18","unstructured":"SMACK software verifier and verification toolchain. http:\/\/smackers.github.io"},{"key":"12_CR19","unstructured":"Translation error of uses of the copysign family of functions #801. https:\/\/github.com\/smackers\/smack\/issues\/801"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:36Z","timestamp":1764401796000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}