[{"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"language":[{"iso":"eng"}],"issue":"2-3","isi":1,"pubrep_id":"656","quality_controlled":"1","doi":"10.1007/s10703-016-0256-5","department":[{"_id":"ToHe"}],"publisher":"Springer","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publication":"Formal Methods in System Design","day":"01","file":[{"file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf","content_type":"application/pdf","relation":"main_file","file_size":1416170,"creator":"system","date_updated":"2020-07-14T12:44:44Z","file_id":"4985","checksum":"1163dfd997e8212c789525d4178b1653","date_created":"2018-12-12T10:13:05Z","access_level":"open_access"}],"author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"full_name":"Clarke, Edmund","last_name":"Clarke","first_name":"Edmund"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun"},{"first_name":"Leonid","last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta"},{"full_name":"Tarrach, Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","last_name":"Tarrach","first_name":"Thorsten"}],"publist_id":"5929","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","status":"public","external_id":{"isi":["000399888900001"]},"citation":{"ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139. doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 50(2–3), 97–139.","mla":"Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer, 2017, pp. 97–139, doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>.","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3. Springer, pp. 97–139, 2017.","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, Formal Methods in System Design 50 (2017) 97–139."},"related_material":{"record":[{"relation":"earlier_version","id":"1729","status":"public"}]},"intvolume":"        50","has_accepted_license":"1","oa":1,"publication_status":"published","ddc":["000"],"date_published":"2017-06-01T00:00:00Z","year":"2017","_id":"1338","abstract":[{"text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.","lang":"eng"}],"date_updated":"2023-09-20T11:13:51Z","month":"06","oa_version":"Published Version","type":"journal_article","page":"97 - 139","file_date_updated":"2020-07-14T12:44:44Z","date_created":"2018-12-11T11:51:27Z","volume":50},{"conference":{"start_date":"2016-01-17","location":"St. Petersburg, FL, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19"},"language":[{"iso":"eng"}],"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"doi":"10.1007/978-3-662-49122-5_12","quality_controlled":"1","ec_funded":1,"scopus_import":1,"publisher":"Springer","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"title":"Lipschitz robustness of timed I/O systems","publist_id":"5647","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha"}],"day":"01","intvolume":"      9583","citation":{"mla":"Henzinger, Thomas A., et al. <i>Lipschitz Robustness of Timed I/O Systems</i>. Vol. 9583, Springer, 2016, pp. 250–67, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>.","ista":"Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 250–267.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2016). Lipschitz robustness of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Timed I/O Systems,” 9583:250–67. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>."},"alternative_title":["LNCS"],"status":"public","date_published":"2016-01-01T00:00:00Z","main_file_link":[{"url":"http://arxiv.org/abs/1506.01233","open_access":"1"}],"publication_status":"published","oa":1,"_id":"1526","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.","year":"2016","volume":9583,"date_created":"2018-12-11T11:52:32Z","page":"250 - 267","type":"conference","oa_version":"Preprint","month":"01","abstract":[{"text":"We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems — timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem.","lang":"eng"}],"date_updated":"2021-01-12T06:51:23Z"},{"quality_controlled":"1","doi":"10.1007/978-3-319-41540-6_21","date_published":"2016-07-13T00:00:00Z","publication_status":"published","citation":{"ieee":"L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 383–401.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>.","short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.","ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>","mla":"D’Antoni, Loris, et al. <i>QLOSE: Program Repair with Quantitative Objectives</i>. Vol. 9780, Springer, 2016, pp. 383–401, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>.","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","apa":"D’Antoni, L., Samanta, R., &#38; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>"},"language":[{"iso":"eng"}],"conference":{"end_date":"2016-07-23","start_date":"2016-07-17","location":"Toronto, Canada","name":"CAV: Computer Aided Verification"},"intvolume":"      9780","status":"public","alternative_title":["LNCS"],"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publist_id":"5819","date_created":"2018-12-11T11:51:45Z","title":"QLOSE: Program repair with quantitative objectives","volume":9780,"oa_version":"None","type":"conference","month":"07","day":"13","abstract":[{"text":"The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect\r\nto a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating\r\nQlose on programs taken from educational tools such as CodeHunt and edX.","lang":"eng"}],"date_updated":"2021-01-12T06:50:21Z","page":"383 - 401","author":[{"full_name":"D'Antoni, Loris","first_name":"Loris","last_name":"D'Antoni"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","last_name":"Samanta","first_name":"Roopsha"},{"last_name":"Singh","first_name":"Rishabh","full_name":"Singh, Rishabh"}],"ec_funded":1,"scopus_import":1,"_id":"1390","department":[{"_id":"ToHe"}],"year":"2016","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Springer"},{"_id":"1729","year":"2015","file_date_updated":"2020-07-14T12:45:13Z","date_created":"2018-12-11T11:53:42Z","volume":9207,"date_updated":"2023-09-20T11:13:50Z","abstract":[{"lang":"eng","text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions."}],"oa_version":"Submitted Version","type":"conference","month":"07","page":"180 - 197","citation":{"ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. 2015;9207:180-197. doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using synchronization synthesis. Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2015. From non-preemptive to preemptive scheduling using synchronization synthesis. 9207, 180–197.","mla":"Cerny, Pavol, et al. <i>From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis</i>. Vol. 9207, Springer, 2015, pp. 180–97, doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>.","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197."},"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"1130"},{"status":"public","id":"1338","relation":"later_version"}]},"intvolume":"      9207","status":"public","alternative_title":["LNCS"],"ddc":["000"],"date_published":"2015-07-01T00:00:00Z","has_accepted_license":"1","publication_status":"published","scopus_import":1,"ec_funded":1,"department":[{"_id":"ToHe"}],"publisher":"Springer","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5398","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","file":[{"date_updated":"2020-07-14T12:45:13Z","file_id":"4715","checksum":"6ff58ac220e2f20cb001ba35d4924495","date_created":"2018-12-12T10:08:53Z","access_level":"local","file_name":"IST-2015-336-v1+1_long_version.pdf","content_type":"application/pdf","relation":"main_file","file_size":481922,"creator":"system"}],"day":"01","author":[{"full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol"},{"full_name":"Clarke, Edmund","first_name":"Edmund","last_name":"Clarke"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun"},{"first_name":"Leonid","last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid"},{"last_name":"Samanta","first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha"},{"orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten","first_name":"Thorsten","last_name":"Tarrach"}],"language":[{"iso":"eng"}],"series_title":"Lecture Notes in Computer Science","conference":{"start_date":"2015-07-18","location":"San Francisco, CA, United States","name":"CAV: Computer Aided Verification","end_date":"2015-07-24"},"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"quality_controlled":"1","doi":"10.1007/978-3-319-21668-3_11","pubrep_id":"336"},{"oa":1,"publication_status":"published","has_accepted_license":"1","date_published":"2015-01-15T00:00:00Z","ddc":["005"],"status":"public","citation":{"chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>.","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444."},"page":"433 - 444","abstract":[{"text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.","lang":"eng"}],"date_updated":"2021-01-12T06:54:33Z","type":"conference","month":"01","oa_version":"Submitted Version","date_created":"2018-12-11T11:55:05Z","file_date_updated":"2020-07-14T12:45:22Z","year":"2015","_id":"1992","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"pubrep_id":"317","doi":"10.1145/2676726.2677008","quality_controlled":"1","conference":{"start_date":"2015-01-15","location":"Mumbai, India","name":"POPL: Principles of Programming Languages","end_date":"2015-01-17"},"language":[{"iso":"eng"}],"author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha"},{"first_name":"Thorsten","last_name":"Tarrach","full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87"}],"day":"15","file":[{"file_name":"IST-2015-317-v1+1_author_version.pdf","creator":"system","relation":"main_file","content_type":"application/pdf","file_size":399462,"checksum":"f0d4395b600f410a191256ac0b73af32","date_updated":"2020-07-14T12:45:22Z","file_id":"5314","access_level":"open_access","date_created":"2018-12-12T10:17:56Z"}],"title":"Succinct representation of concurrent trace sets","publist_id":"5091","publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"scopus_import":1},{"intvolume":"        29","citation":{"mla":"Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>.","ista":"Henzinger TA, Otop J, Samanta R. 2014. Lipschitz robustness of finite-state transducers. Leibniz International Proceedings in Informatics, LIPIcs. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 29, 431–443.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In <i>Leibniz International Proceedings in Informatics, LIPIcs</i> (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: <i>Leibniz International Proceedings in Informatics, LIPIcs</i>. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–443.","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, Delhi, India, 2014, vol. 29, pp. 431–443.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>."},"alternative_title":["LIPIcs"],"status":"public","ddc":["004"],"date_published":"2014-12-01T00:00:00Z","oa":1,"publication_status":"published","has_accepted_license":"1","_id":"1870","year":"2014","volume":29,"date_created":"2018-12-11T11:54:27Z","file_date_updated":"2020-07-14T12:45:19Z","page":"431 - 443","month":"12","type":"conference","oa_version":"Published Version","date_updated":"2021-01-12T06:53:45Z","abstract":[{"lang":"eng","text":"We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers."}],"conference":{"start_date":"2014-12-15","location":"Delhi, India","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2014-12-17"},"language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.FSTTCS.2014.431","quality_controlled":"1","pubrep_id":"804","publication":"Leibniz International Proceedings in Informatics, LIPIcs","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"title":"Lipschitz robustness of finite-state transducers","publist_id":"5227","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha"}],"file":[{"file_name":"IST-2017-804-v1+1_37.pdf","creator":"system","file_size":562151,"relation":"main_file","content_type":"application/pdf","checksum":"7b1aff1710a8bffb7080ec07f62d9a17","file_id":"4734","date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","date_created":"2018-12-12T10:09:11Z"}],"day":"01"},{"intvolume":"      8723","citation":{"mla":"Samanta, Roopsha, et al. <i>Cost-Aware Automatic Program Repair</i>. Edited by Markus Müller-Olm and Helmut Seidl, vol. 8723, Springer, 2014, pp. 268–84, doi:<a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">10.1007/978-3-319-10936-7_17</a>.","ista":"Samanta R, Olivo O, Allen E. 2014. Cost-aware automatic program repair. SAS: Static Analysis Symposium, LNCS, vol. 8723, 268–284.","apa":"Samanta, R., Olivo, O., &#38; Allen, E. (2014). Cost-aware automatic program repair. In M. Müller-Olm &#38; H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented at the SAS: Static Analysis Symposium, Munich, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">https://doi.org/10.1007/978-3-319-10936-7_17</a>","ama":"Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:<a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">10.1007/978-3-319-10936-7_17</a>","short":"R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer, 2014, pp. 268–284.","ieee":"R. Samanta, O. Olivo, and E. Allen, “Cost-aware automatic program repair,” presented at the SAS: Static Analysis Symposium, Munich, Germany, 2014, vol. 8723, pp. 268–284.","chicago":"Samanta, Roopsha, Oswaldo Olivo, and Emerson Allen. “Cost-Aware Automatic Program Repair.” edited by Markus Müller-Olm and Helmut Seidl, 8723:268–84. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">https://doi.org/10.1007/978-3-319-10936-7_17</a>."},"alternative_title":["LNCS"],"editor":[{"last_name":"Müller-Olm","first_name":"Markus","full_name":"Müller-Olm, Markus"},{"first_name":"Helmut","last_name":"Seidl","full_name":"Seidl, Helmut"}],"status":"public","date_published":"2014-09-01T00:00:00Z","ddc":["000","005"],"oa":1,"publication_status":"published","has_accepted_license":"1","_id":"1875","year":"2014","volume":8723,"file_date_updated":"2020-07-14T12:45:19Z","date_created":"2018-12-11T11:54:29Z","page":"268 - 284","date_updated":"2021-01-12T06:53:46Z","abstract":[{"lang":"eng","text":"We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs."}],"month":"09","type":"conference","oa_version":"Submitted Version","conference":{"location":"Munich, Germany","name":"SAS: Static Analysis Symposium","start_date":"2014-09-11","end_date":"2014-09-14"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-10936-7_17","quality_controlled":"1","pubrep_id":"313","scopus_import":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"ToHe"}],"title":"Cost-aware automatic program repair","publist_id":"5221","author":[{"last_name":"Samanta","first_name":"Roopsha","full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Olivo","first_name":"Oswaldo","full_name":"Olivo, Oswaldo"},{"full_name":"Allen, Emerson","last_name":"Allen","first_name":"Emerson"}],"file":[{"file_name":"IST-2014-313-v1+1_SOE.SAS14.pdf","creator":"system","content_type":"application/pdf","relation":"main_file","file_size":409485,"checksum":"78ec4ea1bdecc676cd3e8cad35c6182c","date_updated":"2020-07-14T12:45:19Z","file_id":"4650","access_level":"open_access","date_created":"2018-12-12T10:07:51Z"}],"day":"01"}]