{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T20:59:19Z","timestamp":1757624359258,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","funder":[{"name":"US National Science Foundation (NSF)","award":["2224985"],"award-info":[{"award-number":["2224985"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,7,20]]},"DOI":"10.1145\/3731545.3744151","type":"proceedings-article","created":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T12:46:16Z","timestamp":1757421976000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantum-Based SMT Solving for String Theory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0097-2120","authenticated-orcid":false,"given":"Beatrice","family":"Casey","sequence":"first","affiliation":[{"name":"University of Notre Dame, South Bend, Indiana, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8743-2516","authenticated-orcid":false,"given":"Joanna C. S.","family":"Santos","sequence":"additional","affiliation":[{"name":"University of Notre Dame, South Bend, Indiana, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2189-7497","authenticated-orcid":false,"given":"Andrew","family":"Hennessee","sequence":"additional","affiliation":[{"name":"University of Notre Dame, South Bend, Indiana, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,9,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Satisfiability modulo theories. Handbook of model checking","author":"Barrett Clark","year":"2018","unstructured":"Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. Handbook of model checking, pages 305\u2013343, 2018."},{"key":"e_1_3_2_1_2_1","first-page":"141","article-title":"Lazy satisfiability modulo theories. Journal on Satisfiability","volume":"3","author":"Sebastiani Roberto","year":"2007","unstructured":"Roberto Sebastiani. Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modelling and Computation, 3(3\u20134):141\u2013224, 2007.","journal-title":"Boolean Modelling and Computation"},{"key":"e_1_3_2_1_3_1","first-page":"340","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. Z3: An efficient smt solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337\u2013340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_4_1","volume-title":"Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1\u201339","author":"Baldoni Roberto","year":"2018","unstructured":"Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1\u201339, 2018."},{"issue":"1","key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/1328897.1328461","article-title":"Back to the future: revisiting precise program verification using smt solvers","volume":"43","author":"Lahiri Shuvendu","year":"2008","unstructured":"Shuvendu Lahiri and Shaz Qadeer. Back to the future: revisiting precise program verification using smt solvers. ACM SIGPLAN Notices, 43(1):171\u2013182, 2008.","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-015-9163-z"},{"key":"e_1_3_2_1_7_1","first-page":"304","volume-title":"2008 IEEE Real-Time and Embedded Technology and Applications Symposium","author":"Yuan Mingxuan","year":"2008","unstructured":"Mingxuan Yuan, Xiuqiang He, and Zonghua Gu. Hardware\/software partitioning and static task scheduling on runtime reconfigurable fpgas using a smt solver. In 2008 IEEE Real-Time and Embedded Technology and Applications Symposium, pages 295\u2013304, 2008."},{"key":"e_1_3_2_1_8_1","first-page":"1470","volume-title":"Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, ICSE '20","author":"Bugariu Alexandra","year":"2020","unstructured":"Alexandra Bugariu and Peter M\u00fcller. Automatically testing string solvers. In Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, ICSE '20, page 1459\u20131470, New York, NY, USA, 2020. Association for Computing Machinery."},{"key":"e_1_3_2_1_9_1","volume-title":"A quantum smt solver for bit-vector theory","author":"Lin Shang-Wei","year":"2023","unstructured":"Shang-Wei Lin, Si-Han Chen, Tzu-Fan Wang, and Yean-Ru Chen. A quantum smt solver for bit-vector theory, 2023."},{"key":"e_1_3_2_1_10_1","first-page":"312","volume-title":"Computer Aided Verification","author":"Berzish Murphy","year":"2021","unstructured":"Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, and Vijay Ganesh. An smt solver for regular expressions and linear arithmetic over string length. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 289\u2013312, Cham, 2021. Springer International Publishing."},{"key":"e_1_3_2_1_11_1","first-page":"126","volume-title":"2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C)","author":"Subramanian Sanu","year":"2017","unstructured":"Sanu Subramanian, Murphy Berzish, Omer Tripp, and Vijay Ganesh. A solver for a theory of strings and bit-vectors. In 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C), pages 124\u2013126, 2017."},{"key":"e_1_3_2_1_12_1","volume-title":"The smt-lib format: an initial proposal. 01","author":"Tinelli Cesare","year":"2003","unstructured":"Cesare Tinelli. The smt-lib format: an initial proposal. 01 2003."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"e_1_3_2_1_14_1","first-page":"5","volume-title":"2018 Formal Methods in Computer Aided Design (FMCAD)","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luk\u00e1\u0161 Hol\u00edk, Ahmed Rezine, and Philipp R\u00fcmmer. Trau: Smt solver for string constraints. In 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1\u20135, 2018."},{"key":"e_1_3_2_1_15_1","first-page":"234","volume-title":"Proceedings 15th Annual IEEE Conference on Computational Complexity","author":"Karakostas G.","year":"2000","unstructured":"G. Karakostas, R.J. Lipton, and A. Viglas. On the complexity of intersecting finite state automata. In Proceedings 15th Annual IEEE Conference on Computational Complexity, pages 229\u2013234, 2000."},{"key":"e_1_3_2_1_16_1","volume-title":"Word equations in synergy with regular constraints (technical report)","author":"Blahoudek Franti\u0161ek","year":"2022","unstructured":"Franti\u0161ek Blahoudek, Yu-Fang Chen, David Chocholat\u00fd, Vojt\u011bch Havlena, Luk\u00e1\u0161 Hol\u00edk, Ond\u0159ej Leng\u00e1l, and Juraj S\u00ed\u010d. Word equations in synergy with regular constraints (technical report), 2022."},{"key":"e_1_3_2_1_17_1","unstructured":"Z3.seq. https:\/\/z3prover.github.io\/api\/html\/ml\/Z3.Seq.html."},{"key":"e_1_3_2_1_18_1","first-page":"59","volume-title":"2017 Formal Methods in Computer Aided Design (FMCAD)","author":"Berzish Murphy","unstructured":"Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. Z3str3: A string solver with theory-aware heuristics. In 2017 Formal Methods in Computer Aided Design (FMCAD), pages 55\u201359. IEEE, 2017."},{"key":"e_1_3_2_1_19_1","first-page":"177","volume-title":"Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings 23","author":"Barrett Clark","unstructured":"Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. cvc4. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings 23, pages 171\u2013177. Springer, 2011."},{"issue":"3","key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"94","DOI":"10.3390\/fi15030094","article-title":"Quantum computing for healthcare: A review","volume":"15","author":"Rasool Raihan Ur","year":"2023","unstructured":"Raihan Ur Rasool, Hafiz Farooq Ahmad, Wajid Rafique, Adnan Qayyum, Junaid Qadir, and Zahid Anwar. Quantum computing for healthcare: A review. Future Internet, 15(3):94, 2023.","journal-title":"Future Internet"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1021\/acs.jctc.2c00574"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-023-00603-1"},{"key":"e_1_3_2_1_23_1","volume-title":"IGI Global","author":"Brijwani Geeta N","year":"2023","unstructured":"Geeta N Brijwani, Prafulla E Ajmire, and Pragati V Thawani. Future of quantum computing in cyber security. In Handbook of research on quantum computing for smart environments, pages 267\u2013298. IGI Global, 2023."},{"issue":"5","key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","first-page":"4135","DOI":"10.1109\/TPWRS.2020.3004073","article-title":"Quantum computing for enhancing grid security","volume":"35","author":"Eskandarpour Rozhin","year":"2020","unstructured":"Rozhin Eskandarpour, Pranav Gokhale, Amin Khodaei, Frederic T Chong, Aleksi Passo, and Shay Bahramirad. Quantum computing for enhancing grid security. IEEE Transactions on Power Systems, 35(5):4135\u20134137, 2020.","journal-title":"IEEE Transactions on Power Systems"},{"issue":"1","key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.30574\/msarr.2024.10.1.0038","article-title":"Exploring and reviewing the potential of quantum computing in enhancing cybersecurity encryption methods","volume":"10","author":"Ajala Olakunle Abayomi","year":"2024","unstructured":"Olakunle Abayomi Ajala, Chuka Anthony Arinze, Onyeka Chrisanctus Ofodile, Chinwe Chinazo Okoye, and Andrew Ifesinachi Daraojimba. Exploring and reviewing the potential of quantum computing in enhancing cybersecurity encryption methods. Magna Sci. Adv. Res. Rev, 10(1):321\u2013329, 2024.","journal-title":"Magna Sci. Adv. Res. Rev"},{"key":"e_1_3_2_1_26_1","volume-title":"Entanglement and quantum computation","author":"Jozsa Richard","year":"1997","unstructured":"Richard Jozsa. Entanglement and quantum computation, 1997."},{"key":"e_1_3_2_1_27_1","volume-title":"Jan","author":"Montanaro Ashley","year":"2016","unstructured":"Ashley Montanaro. Quantum algorithms: an overview. npj Quantum Information, 2(1):15023, Jan 2016."},{"key":"e_1_3_2_1_28_1","volume-title":"Quantum computing | d-wave","author":"Systems Wave","year":"2025","unstructured":"D-Wave Systems. Quantum computing | d-wave, 2025. Accessed: 2025-03-14."},{"key":"e_1_3_2_1_29_1","first-page":"662","volume-title":"International Conference on Computer Aided Verification","author":"Liang Tianyi","unstructured":"Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. A dpll (t) theory solver for a theory of strings and regular expressions. In International Conference on Computer Aided Verification, pages 646\u2013662. Springer, 2014."},{"key":"e_1_3_2_1_30_1","first-page":"188","volume-title":"Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13\u201317, 2004. Proceedings 16","author":"Ganzinger Harald","unstructured":"Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Dpll (t): Fast decision procedures. In Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13\u201317, 2004. Proceedings 16, pages 175\u2013188. Springer, 2004."},{"key":"e_1_3_2_1_31_1","volume-title":"Springer Berlin Heidelberg","author":"de Moura Leonardo","year":"2013","unstructured":"Leonardo de Moura and Grant Olney Passmore. The Strategy Challenge in SMT Solving, pages 15\u201344. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9026-1"},{"key":"e_1_3_2_1_33_1","first-page":"76","volume-title":"Proceedings of the Second Workshop on Automated Formal Methods, AFM '07","author":"Finkbeiner Bernd","year":"2007","unstructured":"Bernd Finkbeiner and Sven Schewe. Smt-based synthesis of distributed systems. In Proceedings of the Second Workshop on Automated Formal Methods, AFM '07, page 69\u201376, New York, NY, USA, 2007. Association for Computing Machinery."},{"key":"e_1_3_2_1_34_1","first-page":"293","volume-title":"Runtime Verification","author":"Valapil Vidhya Tekken","year":"2017","unstructured":"Vidhya Tekken Valapil, Sorrachai Yingchareonthawornchai, Sandeep Kulkarni, Eric Torng, and Murat Demirbas. Monitoring partially synchronous distributed systems using smt solvers. In Shuvendu Lahiri and Giles Reger, editors, Runtime Verification, pages 277\u2013293, Cham, 2017. Springer International Publishing."},{"key":"e_1_3_2_1_35_1","volume-title":"Universite de Grenoble I - Joseph Fourier","author":"Tendulkar Pranav","year":"2014","unstructured":"Pranav Tendulkar. Mapping and Scheduling on Multi-core Processors using SMT Solvers. Theses, Universite de Grenoble I - Joseph Fourier, October 2014."},{"issue":"2","key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1049\/iet-qtc.2020.0027","article-title":"Present landscape of quantum computing","volume":"1","author":"Hassija Vikas","year":"2020","unstructured":"Vikas Hassija, Vinay Chamola, Vikas Saxena, Vaibhav Chanana, Prakhar Parashari, Shahid Mumtaz, and Mohsen Guizani. Present landscape of quantum computing. IET Quantum Communication, 1(2):42\u201348, 2020.","journal-title":"IET Quantum Communication"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1002\/net.21751"},{"key":"e_1_3_2_1_38_1","first-page":"62","volume-title":"2020 IEEE International Conference on Quantum Computing and Engineering (QCE)","author":"Tabi Zsolt","unstructured":"Zsolt Tabi, Kareem H. El-Safty, Zsofia Kallus, Peter Haga, Tamas Kozsik, Adam Glos, and Zoltan Zimboras. Quantum optimization for the graph coloring problem with space-efficient embedding. In 2020 IEEE International Conference on Quantum Computing and Engineering (QCE), page 56\u201362. IEEE, October 2020."},{"key":"e_1_3_2_1_39_1","volume-title":"Electron Markets","author":"Rietsche R.","year":"2022","unstructured":"R. Rietsche, C. Dremel, and C. et al. Bosch. Quantum computing. Electron Markets, 2022."},{"key":"e_1_3_2_1_40_1","volume-title":"Proc. ACM Program. Lang., 8(OOPSLA2)","author":"Kang Chan Gu","year":"2024","unstructured":"Chan Gu Kang, Joonghoon Lee, and Hakjoo Oh. Statistical testing of quantum programs via fixed-point amplitude amplification. Proc. ACM Program. Lang., 8(OOPSLA2), October 2024."},{"key":"e_1_3_2_1_41_1","volume-title":"Faster and better quantum software testing through specification reduction and projective measurements","author":"Oldfield Noah H.","year":"2024","unstructured":"Noah H. Oldfield, Christoph Laaber, Tao Yue, and Shaukat Ali. Faster and better quantum software testing through specification reduction and projective measurements, 2024."},{"key":"e_1_3_2_1_42_1","volume-title":"Mitigating noise in quantum software testing using machine learning","author":"Muqeet Asmar","year":"2024","unstructured":"Asmar Muqeet, Tao Yue, Shaukat Ali, and Paolo Arcaini. Mitigating noise in quantum software testing using machine learning, 2024."},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the 11th ACM Conference on Computing Frontiers, CF '14","author":"JavadiAbhari Ali","year":"2014","unstructured":"Ali JavadiAbhari, Shruti Patil, Daniel Kudrow, Jeff Heckey, Alexey Lvov, Frederic T. Chong, and Margaret Martonosi. Scaffcc: a framework for compilation and analysis of quantum computing programs. In Proceedings of the 11th ACM Conference on Computing Frontiers, CF '14, New York, NY, USA, 2014. Association for Computing Machinery."},{"key":"e_1_3_2_1_44_1","volume-title":"Proc. ACM Program. Lang., 8(OOPSLA2)","author":"Jeon Seungmin","year":"2024","unstructured":"Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, and Jeehoon Kang. Quantum probabilistic model checking for time-bounded properties. Proc. ACM Program. Lang., 8(OOPSLA2), October 2024."},{"key":"e_1_3_2_1_45_1","first-page":"133","volume-title":"Reversible Computation","author":"Cantone Domenico","year":"2023","unstructured":"Domenico Cantone, Simone Faro, and Arianna Pavone. Quantum string matching unfolded and extended. In Martin Kutrib and Uwe Meyer, editors, Reversible Computation, pages 117\u2013133, Cham, 2023. Springer Nature Switzerland."},{"key":"e_1_3_2_1_46_1","volume-title":"Feb","author":"Niroula Pradeep","year":"2021","unstructured":"Pradeep Niroula and Yunseong Nam. A quantum algorithm for string matching. npj Quantum Information, 7(1):37, Feb 2021."},{"key":"e_1_3_2_1_47_1","volume-title":"Bridging classical and quantum string matching: A computational reformulation of bit-parallelism","author":"Faro Simone","year":"2025","unstructured":"Simone Faro, Arianna Pavone, and Caterina Viola. Bridging classical and quantum string matching: A computational reformulation of bit-parallelism, 2025."},{"key":"e_1_3_2_1_48_1","first-page":"24","volume-title":"Proceedings of the 2024 Workshop on Quantum Search and Information Retrieval, QUASAR '24","author":"Marino Francesco Pio","year":"2024","unstructured":"Francesco Pio Marino, Simone Faro, and Antonio Scardace. Practical implementation of a quantum string matching algorithm. In Proceedings of the 2024 Workshop on Quantum Search and Information Retrieval, QUASAR '24, page 17\u201324, New York, NY, USA, 2024. Association for Computing Machinery."},{"key":"e_1_3_2_1_49_1","first-page":"259","volume-title":"Xujin Chen and Bo Li","author":"Faro Simone","year":"2024","unstructured":"Simone Faro, Arianna Pavone, and Caterina Viola. Quantum path parallelism: A circuit-based approach to text searching. In Xujin Chen and Bo Li, editors, Theory and Applications of Models of Computation, pages 247\u2013259, Singapore, 2024. Springer Nature Singapore."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.physrep.2024.03.002"},{"key":"e_1_3_2_1_51_1","volume-title":"Solving boolean satisfiability problems with the quantum approximate optimization algorithm","author":"Boulebnane Sami","year":"2022","unstructured":"Sami Boulebnane and Ashley Montanaro. Solving boolean satisfiability problems with the quantum approximate optimization algorithm, 2022."},{"key":"e_1_3_2_1_52_1","first-page":"31","volume-title":"Proceedings of the 1st International Workshop on Quantum Programming for Software Engineering, QP4SE 2022","author":"Miranskyy Andriy","year":"2022","unstructured":"Andriy Miranskyy. Using quantum computers to speed up dynamic testing of software. In Proceedings of the 1st International Workshop on Quantum Programming for Software Engineering, QP4SE 2022, page 26\u201331, New York, NY, USA, 2022. Association for Computing Machinery."}],"event":{"name":"HPDC '25: 34th International Symposium on High-Performance Parallel and Distributed Computing","location":"University of Notre Dame Conference Facilities Notre Dame IN USA","acronym":"HPDC '25","sponsor":["SIGHPC ACM Special Interest Group on High Performance Computing, Special Interest Group on High Performance Computing","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 34th International Symposium on High-Performance Parallel and Distributed Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3731545.3744151","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T12:50:32Z","timestamp":1757422232000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731545.3744151"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,20]]},"references-count":52,"alternative-id":["10.1145\/3731545.3744151","10.1145\/3731545"],"URL":"https:\/\/doi.org\/10.1145\/3731545.3744151","relation":{},"subject":[],"published":{"date-parts":[[2025,7,20]]},"assertion":[{"value":"2025-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}