{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T15:02:37Z","timestamp":1758121357580,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314610","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"874-888","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Computing summaries of string loops in C for better testing and refactoring"],"prefix":"10.1145","author":[{"given":"Timotej","family":"Kapus","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Oren","family":"Ish-Shalom","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Technion, Israel"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"e_1_3_2_2_2_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D . Ullman . 2006 . Compilers : Principles, Techniques, and Tools (2nd ed.). Addison Wesley . Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd ed.). Addison Wesley."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770417"},{"key":"e_1_3_2_2_4_1","unstructured":"The GPyOpt authors. 2016. GPyOpt: A Bayesian Optimization framework in python. http:\/\/github.com\/SheffieldML\/GPyOpt.  The GPyOpt authors. 2016. GPyOpt: A Bayesian Optimization framework in python. http:\/\/github.com\/SheffieldML\/GPyOpt."},{"volume-title":"Proc. of the 17th Formal Methods in Computer-Aided Design (FMCAD'17)","author":"Berzish M.","key":"e_1_3_2_2_5_1","unstructured":"M. Berzish , V. Ganesh , and Y. Zheng . 2017. Z3str3: A String Solver with Theory-aware Heuristics . In Proc. of the 17th Formal Methods in Computer-Aided Design (FMCAD'17) . M. Berzish, V. Ganesh, and Y. Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In Proc. of the 17th Formal Methods in Computer-Aided Design (FMCAD'17)."},{"key":"e_1_3_2_2_6_1","volume-title":"Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08) . Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_2"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_21"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037754"},{"volume-title":"Proc. of the 6th European Conference on Computer Systems (EuroSys'11)","author":"Collingbourne Peter","key":"e_1_3_2_2_11_1","unstructured":"Peter Collingbourne , Cristian Cadar , and Paul H.J. Kelly . 2011. Symbolic Crosschecking of Floating-Point and SIMD Code . In Proc. of the 6th European Conference on Computer Systems (EuroSys'11) . Peter Collingbourne, Cristian Cadar, and Paul H.J. Kelly. 2011. Symbolic Crosschecking of Floating-Point and SIMD Code. In Proc. of the 6th European Conference on Computer Systems (EuroSys'11)."},{"volume-title":"Proc. of the Haifa Verification Conference (HVC'11)","author":"Collingbourne Peter","key":"e_1_3_2_2_12_1","unstructured":"Peter Collingbourne , Cristian Cadar , and Paul H.J. Kelly . 2011. Symbolic Testing of OpenCL Code . In Proc. of the Haifa Verification Conference (HVC'11) . Peter Collingbourne, Cristian Cadar, and Paul H.J. Kelly. 2011. Symbolic Testing of OpenCL Code. In Proc. of the Haifa Verification Conference (HVC'11)."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174802"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594343"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606649"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_3_2_2_18_1","volume-title":"Regression Verification. In Proc. of the 46th Design Automation Conference (DAC'09)","author":"Godlin Benny","year":"2009","unstructured":"Benny Godlin and Ofer Strichman . 2009 . Regression Verification. In Proc. of the 46th Design Automation Conference (DAC'09) . Benny Godlin and Ofer Strichman. 2009. Regression Verification. In Proc. of the 46th Design Automation Conference (DAC'09)."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_2_23_1","volume-title":"Proc. of the joint meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (ESEC\/FSE'13)","author":"Hawblitzel Chris","year":"2013","unstructured":"Chris Hawblitzel , Shuvendu K. Lahiri , Kshama Pawar , Hammad Hashmi , Sedar Gokbulut , Lakshan Fernando , Dave Detlefs , and Scott Wadsworth . 2013 . Will You Still Compile Me Tomorrow? Static Crossversion Compiler Validation . In Proc. of the joint meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (ESEC\/FSE'13) . Chris Hawblitzel, Shuvendu K. Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, and Scott Wadsworth. 2013. Will You Still Compile Me Tomorrow? Static Crossversion Compiler Validation. In Proc. of the joint meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (ESEC\/FSE'13)."},{"volume-title":"Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09)","author":"Kiezun Adam","key":"e_1_3_2_2_24_1","unstructured":"Adam Kiezun , Vijay Ganesh , Philip J. Guo , Pieter Hooimeijer , and Michael D. Ernst . 2009. HAMPI: A Solver for String Constraints . In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09) . Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. 2009. HAMPI: A Solver for String Constraints. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_2_2_28_1","first-page":"3","article-title":"An Efficient SMT Solver for String Constraints","volume":"48","author":"Liang Tianyi","year":"2016","unstructured":"Tianyi Liang , Andrew Reynolds , Nestan Tsiskaridze , Cesare Tinelli , Clark Barrett , and Morgan Deters . 2016 . An Efficient SMT Solver for String Constraints . Formal Methods in System Design (FMSD) 48 , 3 (June 2016), 206-234. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. 2016. An Efficient SMT Solver for String Constraints. Formal Methods in System Design (FMSD) 48, 3 (June 2016), 206-234.","journal-title":"Formal Methods in System Design (FMSD)"},{"volume-title":"Inference & Learning Algorithms","author":"MacKay David J. C.","key":"e_1_3_2_2_29_1","unstructured":"David J. C. MacKay . 2002. Information Theory , Inference & Learning Algorithms . Cambridge University Press . David J. C. MacKay. 2002. Information Theory, Inference & Learning Algorithms. Cambridge University Press."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_2_31_1","volume-title":"Test-driven Synthesis. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'14)","author":"Perelman Daniel","year":"2014","unstructured":"Daniel Perelman , Sumit Gulwani , Dan Grossman , and Peter Provost . 2014 . Test-driven Synthesis. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'14) . Daniel Perelman, Sumit Gulwani, Dan Grossman, and Peter Provost. 2014. Test-driven Synthesis. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'14)."},{"volume-title":"Proc. of the ACM Symposium on the Foundations of Software Engineering (FSE'08)","author":"Person Suzette","key":"e_1_3_2_2_32_1","unstructured":"Suzette Person , Matthew B. Dwyer , Sebastian Elbaum , and Corina S . P?s?reanu. 2008. Differential symbolic execution . In Proc. of the ACM Symposium on the Foundations of Software Engineering (FSE'08) . Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. P?s?reanu. 2008. Differential symbolic execution. In Proc. of the ACM Symposium on the Foundations of Software Engineering (FSE'08)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00117-2"},{"key":"e_1_3_2_2_34_1","volume-title":"Translation Validation. In Proc. of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98)","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli , Michael Siegel , and Eli Singerman . 1998 . Translation Validation. In Proc. of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98) . Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Proc. of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98)."},{"volume-title":"Proc. of the 23rd International Conference on Computer-Aided Verification (CAV'11)","author":"David","key":"e_1_3_2_2_35_1","unstructured":"David A. Ramos and Dawson R. Engler. 2011. Practical, Low-Effort Equivalence Verification of Real Code . In Proc. of the 23rd International Conference on Computer-Aided Verification (CAV'11) . David A. Ramos and Dawson R. Engler. 2011. Practical, Low-Effort Equivalence Verification of Real Code. In Proc. of the 23rd International Conference on Computer-Aided Verification (CAV'11)."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805648"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572299"},{"key":"e_1_3_2_2_39_1","volume-title":"Stochastic Superoptimization. In Proc. of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'13)","author":"Schkufza Eric","year":"2013","unstructured":"Eric Schkufza , Rahul Sharma , and Alex Aiken . 2013 . Stochastic Superoptimization. In Proc. of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'13) . Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic Superoptimization. In Proc. of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'13)."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1308173.1308254"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"volume-title":"Proc. of the IEEE International Conference on Software Testing, Verification, and Validation (ICST'18)","author":"Sharma V.","key":"e_1_3_2_2_42_1","unstructured":"V. Sharma , K. Hietala , and S. McCamant . 2018. Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters . In Proc. of the IEEE International Conference on Software Testing, Verification, and Validation (ICST'18) . V. Sharma, K. Hietala, and S. McCamant. 2018. Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters. In Proc. of the IEEE International Conference on Software Testing, Verification, and Validation (ICST'18)."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_2_45_1","volume-title":"Proceedings of the ACM on Programming Languages 2, OOPSLA, Article 165 (Oct.","author":"Sousa Marcelo","year":"2018","unstructured":"Marcelo Sousa , Isil Dillig , and Shuvendu K. Lahiri . 2018. Verified Three-way Program Merge . Proceedings of the ACM on Programming Languages 2, OOPSLA, Article 165 (Oct. 2018 ), 29 pages. Marcelo Sousa, Isil Dillig, and Shuvendu K. Lahiri. 2018. Verified Three-way Program Merge. Proceedings of the ACM on Programming Languages 2, OOPSLA, Article 165 (Oct. 2018), 29 pages."},{"key":"e_1_3_2_2_46_1","volume-title":"Proc. of the 27th International Conference on International Conference on Machine Learning (ICML'10)","author":"Srinivas Niranjan","year":"2010","unstructured":"Niranjan Srinivas , Andreas Krause , Sham Kakade , and Matthias Seeger . 2010 . Gaussian Process Optimization in the Bandit Setting: No Regret and Experimental Design . In Proc. of the 27th International Conference on International Conference on Machine Learning (ICML'10) . Niranjan Srinivas, Andreas Krause, Sham Kakade, and Matthias Seeger. 2010. Gaussian Process Optimization in the Bandit Setting: No Regret and Experimental Design. In Proc. of the 27th International Conference on International Conference on Machine Learning (ICML'10)."},{"volume-title":"Proc. of the 37th ACM Symposium on the Principles of Programming Languages (POPL'10)","author":"Srivastava Saurabh","key":"e_1_3_2_2_47_1","unstructured":"Saurabh Srivastava , Sumit Gulwani , and Jeffrey S. Foster . 2010. From Program Verification to Program Synthesis . In Proc. of the 37th ACM Symposium on the Principles of Programming Languages (POPL'10) . Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From Program Verification to Program Synthesis. In Proc. of the 37th ACM Symposium on the Principles of Programming Languages (POPL'10)."},{"key":"e_1_3_2_2_48_1","volume-title":"Special issue: program equivalence. Formal Methods in System Design 52, 3 (01","author":"Strichman Ofer","year":"2018","unstructured":"Ofer Strichman . 2018. Special issue: program equivalence. Formal Methods in System Design 52, 3 (01 Jun 2018 ), 227-228. Ofer Strichman. 2018. Special issue: program equivalence. Formal Methods in System Design 52, 3 (01 Jun 2018), 227-228."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_2_51_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL (Dec.","author":"Wang Yuepeng","year":"2017","unstructured":"Yuepeng Wang , Isil Dillig , Shuvendu K. Lahiri , and William R. Cook . 2017. Verifying Equivalence of Database-driven Applications . Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017 ), 56:1-56:29. Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2017. Verifying Equivalence of Database-driven Applications. Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017), 56:1-56:29."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771815"},{"key":"e_1_3_2_2_53_1","volume-title":"Regular Expressions, and Length Constraints. Formal Methods in System Design (FMSD) 50 (June","author":"Zheng Yunhui","year":"2017","unstructured":"Yunhui Zheng , Vijay Ganesh , Sanu Subramanian , Omer Tripp , Murphy Berzish , Julian Dolby , and Xiangyu Zhang . 2017. Z3Str2: An Efficient Solver for Strings , Regular Expressions, and Length Constraints. Formal Methods in System Design (FMSD) 50 (June 2017 ), 249-288. Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Murphy Berzish, Julian Dolby, and Xiangyu Zhang. 2017. Z3Str2: An Efficient Solver for Strings, Regular Expressions, and Length Constraints. Formal Methods in System Design (FMSD) 50 (June 2017), 249-288."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Phoenix AZ USA","acronym":"PLDI '19"},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314610","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314610","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314610"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":54,"alternative-id":["10.1145\/3314221.3314610","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314610","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}