[{"publist_id":"6478","abstract":[{"text":"Recently there has been a proliferation of automated program repair (APR) techniques, targeting various programming languages. Such techniques can be generally classified into two families: syntactic- and semantics-based. Semantics-based APR, on which we focus, typically uses symbolic execution to infer semantic constraints and then program synthesis to construct repairs conforming to them. While syntactic-based APR techniques have been shown successful on bugs in real-world programs written in both C and Java, semantics-based APR techniques mostly target C programs. This leaves empirical comparisons of the APR families not fully explored, and developers without a Java-based semantics APR technique. We present JFix, a semantics-based APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs. It extends one particular APR technique (Angelix), and is designed to be sufficiently generic to support a variety of such techniques. We demonstrate that semantics-based APR can indeed efficiently and effectively repair a variety of classes of bugs in large real-world Java programs. This supports our claim that the framework can both support developers seeking semantics-based repair of bugs in Java programs, as well as enable larger scale empirical studies comparing syntactic- and semantics-based APR targeting Java. The demonstration of our tool is available via the project website at: https://xuanbachle.github.io/semanticsrepair/ ","lang":"eng"}],"type":"conference","oa_version":"None","date_updated":"2021-01-12T08:22:05Z","date_created":"2018-12-11T11:49:19Z","author":[{"full_name":"Le, Xuan","last_name":"Le","first_name":"Xuan"},{"full_name":"Chu, Duc Hiep","last_name":"Chu","first_name":"Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"first_name":"David","last_name":"Lo","full_name":"Lo, David"},{"full_name":"Le Goues, Claire","first_name":"Claire","last_name":"Le Goues"},{"last_name":"Visser","first_name":"Willem","full_name":"Visser, Willem"}],"publisher":"ACM","department":[{"_id":"ToHe"}],"publication_status":"published","status":"public","title":"JFIX: Semantics-based repair of Java programs via symbolic PathFinder","year":"2017","_id":"941","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"07","day":"10","scopus_import":1,"language":[{"iso":"eng"}],"doi":"10.1145/3092703.3098225","date_published":"2017-07-10T00:00:00Z","conference":{"start_date":"2017-07-10","location":"Santa Barbara, CA, United States","end_date":"2017-07-14","name":"ISSTA: International Symposium on Software Testing and Analysis"},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"page":"376 - 379 ","quality_controlled":"1","citation":{"ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2017:376-379. doi:10.1145/3092703.3098225","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA: International Symposium on Software Testing and Analysis, 376–379.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 376–379). Santa Barbara, CA, United States: ACM. https://doi.org/10.1145/3092703.3098225","ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “JFIX: Semantics-based repair of Java programs via symbolic PathFinder,” in Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, United States, 2017, pp. 376–379.","mla":"Le, Xuan, et al. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–79, doi:10.1145/3092703.3098225.","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–379.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, 376–79. ACM, 2017. https://doi.org/10.1145/3092703.3098225."},"publication":"Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis"},{"publist_id":"6443","date_updated":"2023-09-22T09:58:02Z","date_created":"2018-12-11T11:49:26Z","volume":10427,"author":[{"full_name":"Trinh, Minh","last_name":"Trinh","first_name":"Minh"},{"full_name":"Chu, Duc Hiep","first_name":"Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jaffar, Joxan","last_name":"Jaffar","first_name":"Joxan"}],"publication_status":"published","department":[{"_id":"ToHe"}],"editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"publisher":"Springer","year":"2017","month":"01","publication_identifier":{"issn":["03029743"]},"language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany","start_date":"2017-07-24","end_date":"2017-07-28"},"doi":"10.1007/978-3-319-63390-9_21","isi":1,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000431900900021"]},"abstract":[{"text":"We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","oa_version":"None","status":"public","title":"Model counting for recursively-defined strings","intvolume":" 10427","_id":"962","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"01","article_processing_charge":"No","scopus_import":"1","date_published":"2017-01-01T00:00:00Z","page":"399 - 418","citation":{"mla":"Trinh, Minh, et al. Model Counting for Recursively-Defined Strings. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:10.1007/978-3-319-63390-9_21.","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418.","chicago":"Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_21.","ama":"Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","ieee":"M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 399–418.","apa":"Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21"}},{"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000414279300055"]},"language":[{"iso":"eng"}],"doi":"10.1145/3106237.3106309","conference":{"start_date":"2017-09-04","location":"Paderborn, Germany","end_date":"2017-09-08","name":"FSE: Foundations of Software Engineering"},"publication_identifier":{"isbn":["978-145035105-8"]},"month":"09","department":[{"_id":"ToHe"}],"publisher":"ACM","publication_status":"published","year":"2017","volume":"F130154","date_created":"2018-12-11T11:49:19Z","date_updated":"2023-09-26T15:38:36Z","author":[{"full_name":"Le, Xuan","last_name":"Le","first_name":"Xuan"},{"full_name":"Chu, Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87","last_name":"Chu","first_name":"Duc Hiep"},{"full_name":"Lo, David","last_name":"Lo","first_name":"David"},{"full_name":"Le Goues, Claire","last_name":"Le Goues","first_name":"Claire"},{"last_name":"Visser","first_name":"Willem","full_name":"Visser, Willem"}],"publist_id":"6477","page":"593 - 604","citation":{"mla":"Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309.","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,” F130154:593–604. ACM, 2017. https://doi.org/10.1145/3106237.3106309.","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604. doi:10.1145/3106237.3106309","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided repair synthesis via programming by examples. FSE: Foundations of Software Engineering vol. F130154, 593–604.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). S3: Syntax- and semantic-guided repair synthesis via programming by examples (Vol. F130154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM. https://doi.org/10.1145/3106237.3106309","ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “S3: Syntax- and semantic-guided repair synthesis via programming by examples,” presented at the FSE: Foundations of Software Engineering, Paderborn, Germany, 2017, vol. F130154, pp. 593–604."},"date_published":"2017-09-01T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"01","title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"942","oa_version":"None","type":"conference","abstract":[{"text":"A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration-based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. ","lang":"eng"}]}]