{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:58Z","timestamp":1776333478820,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100006374","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2247754"],"award-info":[{"award-number":["CNS-2247754"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,8,6]]},"DOI":"10.1145\/3676642.3736123","type":"proceedings-article","created":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T22:19:59Z","timestamp":1754518799000},"page":"195-211","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["<scp>SYL<\/scp>\n            Q-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7764-5715","authenticated-orcid":false,"given":"Kaki","family":"Ryan","sequence":"first","affiliation":[{"name":"University of North Carolina at Chapel Hill, Chapel Hill, North Carolina, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3930-7440","authenticated-orcid":false,"given":"Cynthia","family":"Sturton","sequence":"additional","affiliation":[{"name":"University of North Carolina at Chapel Hill, Chapel Hill, North Carolina, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,8,6]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Redis community edition. https:\/\/redis.io\/docs\/latest\/get-started\/. Accessed: 2024-10-17."},{"key":"e_1_3_2_1_2_1","unstructured":"Slang. https:\/\/github.com\/MikePopoloski\/slang. Accessed: 2024-10-17."},{"key":"e_1_3_2_1_3_1","unstructured":"SoC vulnerability database. http:\/\/cad4security.org\/index.php\/riscv-vulnerability-details\/. Accessed: 2024-10-17."},{"key":"e_1_3_2_1_4_1","unstructured":"Surelog. https:\/\/github.com\/chipsalliance\/Surelog. Accessed: 2024-10-18."},{"key":"e_1_3_2_1_5_1","unstructured":"SymbiYosys. https:\/\/github.com\/YosysHQ\/sby. Accessed: 2022-11-21."},{"key":"e_1_3_2_1_6_1","unstructured":"Synlig. https:\/\/github.com\/chipsalliance\/synlig. Accessed: 2024-10-18."},{"key":"e_1_3_2_1_7_1","unstructured":"Verific design automation. https:\/\/www.verific.com\/. Accessed: 2024-10-18."},{"key":"e_1_3_2_1_8_1","unstructured":"Yosys. https:\/\/github.com\/YosysHQ\/Yosys. Accessed: 2022-11-21."},{"key":"e_1_3_2_1_9_1","volume-title":"Verifying hardware security modules with Information-Preserving refinement","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying hardware security modules with Information-Preserving refinement. In OSDI. USENIX Association, 2022."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277186"},{"key":"e_1_3_2_1_12_1","unstructured":"Nikolaj Bj\u00f8rner and Lev Nachmanson. Navigating the universe of z3 theory solvers."},{"key":"e_1_3_2_1_13_1","first-page":"1","volume-title":"Automation &#38","author":"Bruns Niklas","year":"2023","unstructured":"Niklas Bruns, Vladimir Herdt, and Rolf Drechsler. Processor verification using symbolic execution: A risc-v case-study. In 2023 Design, Automation &#38; Test in Europe Conference &#38; Exhibition (DATE), pages 1-6, 2023."},{"key":"e_1_3_2_1_14_1","volume-title":"8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of High-Coverage tests for complex systems programs. In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 08), San Diego, CA, December 2008. USENIX Association."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_2_1_16_1","first-page":"1361","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Chen Chen","year":"2023","unstructured":"Chen Chen, Rahul Kande, Nathan Nguyen, Flemming Andersen, Aakash Tyagi, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran. HyPFuzz: Formal-Assisted processor fuzzing. In 32nd USENIX Security Symposium (USENIX Security 23), pages 1361-1378, Anaheim, CA, August 2023. USENIX Association."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3678722.3685536"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/AsianHOST56390.2022.10022071"},{"key":"e_1_3_2_1_20_1","volume-title":"Stanford","author":"Ganesh Vijay","year":"2005","unstructured":"Vijay Ganesh, Sergey Berezin, and David L. Dill. Technical report: A decision procedure for fixed-width bit-vectors. Technical report, Stanford, 2005."},{"key":"e_1_3_2_1_21_1","unstructured":"Hack@DAC. https:\/\/www.dac.com\/Conference\/HackDAC. [Accessed: 2024-04-23]."},{"key":"e_1_3_2_1_22_1","unstructured":"Hack@DAC 2018 Phase 2 Buggy SoC."},{"key":"e_1_3_2_1_23_1","unstructured":"Hack@DAC 2019 Alpha Stage SoC."},{"key":"e_1_3_2_1_24_1","volume-title":"Symbolic trajectory evaluation","author":"Hazelhurst Scott","year":"1996","unstructured":"Scott Hazelhurst and Carl-Johan H. Seger. Symbolic trajectory evaluation, 1996."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694366"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00103"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_32"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_29_1","first-page":"1","volume-title":"ICAAD","author":"Laeufer Kevin","year":"2018","unstructured":"Kevin Laeufer, Jack Koenig, Donggyu Kim, Jonathan Bachrach, and Koushik Sen. RFUZZ: Coverage-Directed Fuzz Testing of RTL on FPGAs. In ICAAD, pages 1-8, 2018."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.2997644"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3066560"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2023.3251954"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415709"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530673"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"e_1_3_2_1_37_1","volume-title":"SecDev","author":"Rogers Jayden","year":"2025","unstructured":"Jayden Rogers, Niyaz Shakeel, Divya Mankani, Samantha Espinosa, Cade Chabra, Kaki Ryan, and Cynthia Sturton. Hardware security benchmarks for open-source systemverilog designs. In SecDev. IEEE, 2025."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623652.3623666"},{"key":"e_1_3_2_1_39_1","first-page":"110","volume-title":"Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD)","author":"Ryan Kaki","year":"2023","unstructured":"Kaki Ryan and Cynthia Sturton. Sylvia: Countering the path explosion problem in the symbolic execution of hardware designs. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 110-121, New York, NY, USA, 2023. TU Wien Academic Press."},{"key":"e_1_3_2_1_40_1","volume-title":"Basilisk: An end-to-end open-source linux-capable risc-v soc in 130nm cmos","author":"Scheffler Paul","year":"2024","unstructured":"Paul Scheffler, Philippe Sauter, Thomas Benz, Frank K. G\u00fcrkaynak, and Luca Benini. Basilisk: An end-to-end open-source linux-capable risc-v soc in 130nm cmos, 2024."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2011916"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383966"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3660817"},{"key":"e_1_3_2_1_44_1","first-page":"267","article-title":"Symbolic execution based test-patterns generation algorithm for hardware trojan detection. Computers &#38;","volume":"78","author":"Shen Lixiang","year":"2018","unstructured":"Lixiang Shen, Dejun Mu, Guo Cao, Maoyuan Qin, Jeremy Blackstone, and Ryan Kastner. Symbolic execution based test-patterns generation algorithm for hardware trojan detection. Computers &#38; Security, 78:267-280, 2018.","journal-title":"Security"},{"key":"e_1_3_2_1_45_1","volume-title":"sv2v","author":"Snow Zachary","year":"2020","unstructured":"Zachary Snow. sv2v, 2020."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16214-0_42"},{"key":"e_1_3_2_1_47_1","first-page":"3237","volume-title":"USENIX '22)","author":"Trippel Timothy","year":"2022","unstructured":"Timothy Trippel, Kang G. Shin, Alex Chernyakhovsky, Garret Kelly, Dominic Rizzo, and Matthew Hicks. Fuzzing Hardware Like Software. In USENIX '22), pages 3237-3254, Boston, MA, August 2022. USENIX Association."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_2_1_49_1","volume-title":"Directed Test Generation for Activation of Security Assertions in RTL Models. ACM Trans. Des. Autom. Electron. Syst., 26(4), jan","author":"Witharana Hasini","year":"2021","unstructured":"Hasini Witharana, Yangdi Lyu, and Prabhat Mishra. Directed Test Generation for Activation of Security Assertions in RTL Models. ACM Trans. Des. Autom. Electron. Syst., 26(4), jan 2021."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00071"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037734"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00030"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICIEA.2016.7603701"}],"event":{"name":"ASPLOS '25: 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Rotterdam Netherlands","acronym":"ASPLOS '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676642.3736123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:24:08Z","timestamp":1757543048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676642.3736123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,6]]},"references-count":53,"alternative-id":["10.1145\/3676642.3736123","10.1145\/3676642"],"URL":"https:\/\/doi.org\/10.1145\/3676642.3736123","relation":{},"subject":[],"published":{"date-parts":[[2025,8,6]]},"assertion":[{"value":"2025-08-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}