{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T21:02:18Z","timestamp":1772830938844,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:00:00Z","timestamp":1719100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100011185","name":"Institute of Software, Chinese Academy of Sciences","doi-asserted-by":"publisher","award":["ISCAS-JCZD-202307"],"award-info":[{"award-number":["ISCAS-JCZD-202307"]}],"id":[{"id":"10.13039\/501100011185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,6,23]]},"DOI":"10.1145\/3649329.3655958","type":"proceedings-article","created":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T19:27:22Z","timestamp":1731007642000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7625-2439","authenticated-orcid":false,"given":"Yufeng","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences, Beijing, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8099-2035","authenticated-orcid":false,"given":"Qiusong","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1897-7536","authenticated-orcid":false,"given":"Yiwei","family":"Ci","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7286-1144","authenticated-orcid":false,"given":"Enyuan","family":"Tian","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences, Beijing, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2024,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Model checking","author":"Clarke Edmund M","unstructured":"Edmund M Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model checking. MIT press."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055616"},{"key":"e_1_3_2_1_3_1","volume-title":"FMCAD.","author":"Berezin Sergey","unstructured":"Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zhu. 1998. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In FMCAD. Vol. 1522. Springer, 369--386."},{"key":"e_1_3_2_1_4_1","volume-title":"International Conference on Computer Aided Verification. Springer, 42--58","author":"Alastair","unstructured":"Alastair Reid et al. 2016. End-to-end verification of processors with isa-formal. In International Conference on Computer Aided Verification. Springer, 42--58."},{"key":"e_1_3_2_1_5_1","unstructured":"Clifford Wolf. 2018. Risc-v formal verification framework. https:\/\/github.com\/YosysHQ\/riscv-formal. (2018)."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834401"},{"key":"e_1_3_2_1_7_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1000--1005","author":"Eshan","unstructured":"Eshan Singh et al. 2019. Symbolic qed pre-silicon verification for automotive microcontroller cores: industrial case study. In 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1000--1005."},{"key":"e_1_3_2_1_8_1","volume-title":"2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 1--8.","author":"Lonsing Florian","year":"2019","unstructured":"Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, and Clark Barrett. 2019. Unlocking the power of formal hardware verification with cosa and symbolic qed. In 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 1--8."},{"key":"e_1_3_2_1_9_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 526--531","author":"Devarajegowda Keerthikumara","year":"2020","unstructured":"Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolfgang Kunz. 2020. Gap-free processor verification by s 2 qed and property generation. In 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 526--531."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SoC.2018.8644957"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993506"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3168821"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2334301"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without bdds. In Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference TACAS'99 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS'99 Amsterdam The Netherlands March 22--28 1999 Proceedings 5. Springer 193--207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Andrew Waterman Yunsup Lee David Patterson Krste Asanovic Volume I User level Isa Andrew Waterman Yunsup Lee and David Patterson. 2014. The risc-v instruction set manual. Volume I: User-Level ISA' version 2.","DOI":"10.21236\/ADA605735"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"e_1_3_2_1_19_1","unstructured":"Clifford Wolf. 2016. Yosys open synthesis suite. (2016)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9\\_22"}],"event":{"name":"DAC '24: 61st ACM\/IEEE Design Automation Conference","location":"San Francisco CA USA","acronym":"DAC '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 61st ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3655958","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649329.3655958","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:55Z","timestamp":1750295875000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3655958"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,23]]},"references-count":20,"alternative-id":["10.1145\/3649329.3655958","10.1145\/3649329"],"URL":"https:\/\/doi.org\/10.1145\/3649329.3655958","relation":{},"subject":[],"published":{"date-parts":[[2024,6,23]]},"assertion":[{"value":"2024-11-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}