{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T06:42:48Z","timestamp":1770964968306,"version":"3.50.1"},"reference-count":40,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603019","type":"proceedings-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T20:33:52Z","timestamp":1546979632000},"page":"1-10","source":"Crossref","is-referenced-by-count":15,"title":["A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4"],"prefix":"10.23919","author":[{"given":"Heiko","family":"Becker","sequence":"first","affiliation":[]},{"given":"Nikita","family":"Zyuzin","sequence":"additional","affiliation":[]},{"given":"Raphael","family":"Monat","sequence":"additional","affiliation":[]},{"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[]},{"given":"Anthony","family":"Fox","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"A New Verified Compiler Backend for CakeML","author":"tan","year":"2016","journal-title":"International Conference on Functional Programming (ICFP)"},{"key":"ref38","article-title":"Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions","author":"solovyev","year":"2015","journal-title":"International Symposium of Formal Methods"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_20"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-3-319-66266-4_14","article-title":"Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis","author":"moscato","year":"2017","journal-title":"Int Conf on Computer Safety Reliability and Security (SAFECOMP)"},{"key":"ref31","author":"moore","year":"1966","journal-title":"Interval Analysis"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"ref37","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-38088-4_26","article-title":"Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations","author":"solovyev","year":"2013"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_23"},{"key":"ref35","article-title":"A Unified Coq Framework for Verifying C Programs with Floating-Point Computations","author":"ramananandro","year":"2016","journal-title":"Certified Programs and Proofs"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364545"},{"key":"ref10","author":"darulova","year":"2015","journal-title":"Rosa - The real compiler"},{"key":"ref40","article-title":"A Formal Model of IEEE Floating Point Arithmetic","author":"yu","year":"2013","journal-title":"Archive of Formal Proofs"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"ref13","first-page":"270","article-title":"Daisy-Framework for Analysis and Optimization of Numerical Programs (Tool Paper)","author":"darulova","year":"2018","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1141277.1141584"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1023\/B:NUMA.0000049462.70970.b6"},{"key":"ref17","author":"fox","year":"2017","journal-title":"A formal model of IEEE floating point arithmetic"},{"key":"ref18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18275-4_17","article-title":"Static Analysis of Finite Precision Computations","author":"goubault","year":"2011","journal-title":"Verification Model Checking and Abstract Interpretation (VMCAI)"},{"key":"ref19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-03542-0_4","article-title":"Robustness Analysis of Finite Precision Implementations","author":"goubault","year":"2013","journal-title":"Asian Symposium on Programming Languages and Systems (APLAS)"},{"key":"ref28","article-title":"A New Extraction for Coq","author":"letouzey","year":"2002","journal-title":"Proc Int Workshop Types Proofs Programs (TYPES)"},{"key":"ref4","author":"becker","year":"2018","journal-title":"A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772987"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/781151.781153"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9317-x"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9255-4"},{"key":"ref2","article-title":"CertiCoq: A Verified Compiler for Coq","author":"anand","year":"2017","journal-title":"Coq for Programming Languages (CoqPL)"},{"key":"ref9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-89330-1_2","article-title":"A Sound Floating-Point Polyhedra Abstract Domain","author":"chen","year":"2008","journal-title":"Asian Symposium on Programming Languages and Systems (APLAS)"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-2256-8"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008712907154"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693164"},{"key":"ref21","year":"2008","journal-title":"IEEE Standard for Floating-Point Arithmetic"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.10.010"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102236"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"ref25","article-title":"Apron: A Library of Numerical Abstract Domains for Static Analysis","author":"jeannet","year":"2009","journal-title":"Computer Aided Verification (CAV)"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603019.pdf?arnumber=8603019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,25]],"date-time":"2022-01-25T20:47:11Z","timestamp":1643143631000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603019\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":40,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603019","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}