{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,29]],"date-time":"2025-08-29T10:41:28Z","timestamp":1756464088690,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_33","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"551-558","source":"Crossref","is-referenced-by-count":6,"title":["Equivalence Checking of a Floating-Point Unit Against a High-Level C Model"],"prefix":"10.1007","author":[{"given":"Rajdeep","family":"Mukherjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saurabh","family":"Joshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Griesmayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., Janssen, G.: Scalable sequential equivalence checking across arbitrary design transformations. In: ICCD, pp. 259\u2013266. IEEE (2006)","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"33_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Brand, D.: Verification of large synthesized designs. In: ICCAD, pp. 534\u2013537 (1993)","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"33_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX (2008)"},{"issue":"2","key":"33_CR5","doi-asserted-by":"crossref","first-page":"10:1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 10:1\u201310:38 (2008). Article No.10","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Proceedings of the 2003 Asia and South Pacific Design Automation Conference, ASP-DAC, pp. 308\u2013311. ACM (2003)","DOI":"10.1145\/1119772.1119831"},{"issue":"3","key":"33_CR7","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"LA Clarke","year":"1976","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215\u2013222 (1976)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys, pp. 315\u2013328 (2011)","DOI":"10.1145\/1966445.1966475"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: POPL, pp. 25\u201335. ACM (1989)","DOI":"10.1145\/75277.75280"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: DATE, pp. 618\u2013623. IEEE (1998)","DOI":"10.1109\/DATE.1998.655922"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-61474-5_66","volume-title":"Computer Aided Verification","author":"M Fujita","year":"1996","unstructured":"Fujita, M.: Verification of arithmetic circuits by comparing two similar circuits. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 159\u2013168. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61474-5_66"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: DATE, pp. 196\u2013201. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090657"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: PLDI, pp. 193\u2013204 (2012)","DOI":"10.1145\/2254064.2254088"},{"key":"33_CR17","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Joshi, S., Griesmayer, A., Kroening, D., Melham, T.: Equivalence checking a floating-point unit against a high-level C model: extended version. Computing Research Repository arXiv:1609.00169 [cs.SE], September 2016","DOI":"10.1007\/978-3-319-48989-6_33"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Wu, W., Hsiao, M.S.: Mining global constraints for improving bounded sequential equivalence checking. In: DAC, pp. 743\u2013748. ACM (2006)","DOI":"10.1145\/1146909.1147098"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Xue, B., Chatterjee, P., Shukla, S.K.: Simplification of C-RTL equivalent checking for fused multiply add unit using intermediate models. In: ASP-DAC, pp. 723\u2013728. IEEE (2013)","DOI":"10.1109\/ASPDAC.2013.6509686"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:30:35Z","timestamp":1749691835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}