{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:42:18Z","timestamp":1770280938820,"version":"3.49.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,11]]},"DOI":"10.1109\/fmcad.2009.5351141","type":"proceedings-article","created":{"date-parts":[[2009,12,11]],"date-time":"2009-12-11T18:55:16Z","timestamp":1260557716000},"page":"69-76","source":"Crossref","is-referenced-by-count":46,"title":["Mixed abstractions for floating-point arithmetic"],"prefix":"10.1109","author":[{"given":"Angelo","family":"Brillout","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","year":"0"},{"key":"17","year":"0"},{"key":"18","year":"0"},{"key":"15","first-page":"3","article-title":"A case study in fomal verification of register-transfer logic with ACL2: The floating point adder of the AMD AthlonTM processor","author":"russinoff","year":"2000","journal-title":"FMCAD '00 Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design"},{"key":"16","year":"0"},{"key":"13","year":"0"},{"key":"14","year":"0"},{"key":"11","year":"0"},{"key":"12","year":"0"},{"key":"21","year":"0"},{"key":"20","year":"0"},{"key":"22","year":"0"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24738-8_18"},{"key":"24","year":"0"},{"key":"25","year":"0"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1613-y"},{"key":"27","year":"0"},{"key":"3","year":"0"},{"key":"2","year":"0"},{"key":"10","article-title":"Interpretation of IEEE-854 floating-point standard and definition in the HOL system","author":"carreno","year":"1995"},{"key":"1","author":"gander","year":"2005","journal-title":"Heisenberg effects in computer-arithmetic"},{"key":"7","year":"0","journal-title":"(SNU Real-Time Benchmarks)"},{"key":"6","year":"0"},{"key":"5","first-page":"118","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"4","year":"0"},{"key":"9","year":"0"},{"key":"8","year":"0"}],"event":{"name":"2009 Formal Methods in Computer-Aided Design (FMCAD)","location":"Austin, TX, USA","start":{"date-parts":[[2009,11,15]]},"end":{"date-parts":[[2009,11,18]]}},"container-title":["2009 Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5344684\/5351113\/05351141.pdf?arnumber=5351141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,19]],"date-time":"2017-03-19T02:20:14Z","timestamp":1489890014000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5351141\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2009.5351141","relation":{},"subject":[],"published":{"date-parts":[[2009,11]]}}}