{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:58:34Z","timestamp":1740131914403,"version":"3.37.3"},"reference-count":33,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2021,5,1]],"date-time":"2021-05-01T00:00:00Z","timestamp":1619827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"name":"Swiss SNF","award":["CloSE (200021_149997\/1)"],"award-info":[{"award-number":["CloSE (200021_149997\/1)"]}]},{"name":"Italian MIUR PRIN project GAUSS","award":["2015KWREMX"],"award-info":[{"award-number":["2015KWREMX"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2021,5,1]]},"DOI":"10.1109\/tse.2019.2898199","type":"journal-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T19:29:55Z","timestamp":1554406195000},"page":"948-968","source":"Crossref","is-referenced-by-count":3,"title":["Reusing Solutions Modulo Theories"],"prefix":"10.1109","volume":"47","author":[{"given":"Andrea","family":"Aquino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7566-8051","authenticated-orcid":false,"given":"Giovanni","family":"Denaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mauro","family":"Pezze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0263-6"},{"key":"ref32","first-page":"153","article-title":"Agrep—A fast approximate pattern-matching tool","author":"wu","year":"1992","journal-title":"Proc Usenix Tech Conf"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"ref11","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc Symp Oper Syst Des Implementation"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"article-title":"Reusing constraint proofs in symbolic analysis","year":"2018","author":"chen","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2011.98"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092728"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/362686.362692"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2881025.2881032"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.46"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092715"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1142\/9789812819536_0023"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786842"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771802"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"year":"2017","author":"aquino","key":"ref1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"ref22","article-title":"Binary codes capable of correcting deletions, insertions, and reversals","volume":"10","author":"levenshtein","year":"1966","journal-title":"Soviet Physics Doklady"},{"journal-title":"Combinatorial Algorithms The Art of Computer Programming","year":"2011","author":"knuth","key":"ref21"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_21"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2623623"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9430779\/08681653.pdf?arnumber=8681653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T19:58:37Z","timestamp":1639771117000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8681653\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,1]]},"references-count":33,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/tse.2019.2898199","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2021,5,1]]}}}