{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T14:16:22Z","timestamp":1760710582598,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,5,10]],"date-time":"2021-05-10T00:00:00Z","timestamp":1620604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2018YFB1308601"],"award-info":[{"award-number":["2018YFB1308601"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSF of China","doi-asserted-by":"crossref","award":["61672310 and 62072267"],"award-info":[{"award-number":["61672310 and 62072267"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100007162","name":"Guangdong Science and Technology Department","doi-asserted-by":"crossref","award":["2018B010107004"],"award-info":[{"award-number":["2018B010107004"]}],"id":[{"id":"10.13039\/501100007162","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>\n            <jats:bold>Satisfiability modulo theories (SMT)<\/jats:bold>\n            solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.\n          <\/jats:p>","DOI":"10.1145\/3446211","type":"journal-article","created":{"date-parts":[[2021,5,10]],"date-time":"2021-05-10T22:17:21Z","timestamp":1620685041000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Leveraging Control Flow Knowledge in SMT Solving of Program Verification"],"prefix":"10.1145","volume":"30","author":[{"given":"Jianhui","family":"Chen","sequence":"first","affiliation":[{"name":"School of Software, Tsinghua University and Key Laboratory for Information System Security, MoE and Beijing National Research Center for Information Science and Technology, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4266-875X","authenticated-orcid":false,"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University and Key Laboratory for Information System Security, MoE and Beijing National Research Center for Information Science and Technology, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,5,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595762"},{"volume-title":"Z3str3: A string solver with theory-aware branching. arXiv preprint arXiv:1704.07935","year":"2017","author":"Berzish Murphy","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"volume-title":"Frontiers in Artificial Intelligence and Applications","year":"2009","author":"Biere Armin","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_23"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238218"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351149"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"volume-title":"Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 25--35","author":"Cytron Ron","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_26"},{"volume-title":"Enderton","year":"2001","author":"Enderton Herbert","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41591-8_6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.17"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776040"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859080"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531077"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48159-1_5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886670"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_23"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-7315(88)90013-5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46135-3_13"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.462.0265"},{"key":"e_1_2_1_39_1","article-title":"A survey on automatic test case generation","volume":"15","author":"Prasanna M.","year":"2005","journal-title":"Academic Open Internet Journal"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/026\/23"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964028"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_36"},{"volume-title":"SAT 2005","year":"2005","author":"Sorensson Niklas","key":"e_1_2_1_43_1"},{"volume-title":"On the complexity of derivation in propositional calculus. Studies in Constrained Mathematics and Mathematical Logic","year":"1968","author":"Tseitin G.","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996713"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.11"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3446211","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3446211","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:04Z","timestamp":1750193224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3446211"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,10]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3446211"],"URL":"https:\/\/doi.org\/10.1145\/3446211","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2021,5,10]]},"assertion":[{"value":"2020-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}