{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T04:03:18Z","timestamp":1763179398848,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":77,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"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":[[2022,7,18]]},"DOI":"10.1145\/3533767.3534369","type":"proceedings-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T14:28:50Z","timestamp":1657895330000},"page":"666-677","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["ATR: template-based repair for Alloy specifications"],"prefix":"10.1145","author":[{"given":"Guolong","family":"Zheng","sequence":"first","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}]},{"given":"ThanhVu","family":"Nguyen","sequence":"additional","affiliation":[{"name":"George Mason University, USA"}]},{"given":"Sim\u00f3n Guti\u00e9rrez","family":"Brida","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Argentina \/ CONICET, Argentina"}]},{"given":"Germ\u00e1n","family":"Regis","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Argentina"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Argentina \/ CONICET, Argentina"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[{"name":"Buenos Aires Institute of Technology, Argentina"}]},{"given":"Hamid","family":"Bagheri","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2020. ExCAPE project. https:\/\/excape.cis.upenn.edu\/ \t\t\t\t\t  2020. ExCAPE project. https:\/\/excape.cis.upenn.edu\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2020. SyGuS. https:\/\/sygus.org\/ \t\t\t\t\t  2020. SyGuS. https:\/\/sygus.org\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397347"},{"key":"e_1_3_2_1_5_1","volume-title":"Mohamad Sakr, and Jad Saklawi.","author":"Attie Paul","year":"2015","unstructured":"Paul Attie , Ali Cherri , Kinan Dak Al Bab , Mohamad Sakr, and Jad Saklawi. 2015 . Model and program repair via sat solving. In MEMOCODE. 148\u2013157. Paul Attie, Ali Cherri, Kinan Dak Al Bab, Mohamad Sakr, and Jad Saklawi. 2015. Model and program repair via sat solving. In MEMOCODE. 148\u2013157."},{"key":"e_1_3_2_1_6_1","first-page":"19248","volume-title":"Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. In FM 2015: Formal Methods (Lecture Notes in Computer Science","volume":"89","author":"Bagheri Hamid","year":"2015","unstructured":"Hamid Bagheri , Eunsuk Kang , Sam Malek , and Daniel Jackson . 2015 . Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. In FM 2015: Formal Methods (Lecture Notes in Computer Science , Vol. 9109). 73\u2013 89 . isbn:978-3-319- 19248 - 19242 Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. 2015. Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. In FM 2015: Formal Methods (Lecture Notes in Computer Science, Vol. 9109). 73\u201389. isbn:978-3-319-19248-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0445-z"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377816.3381728"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2016.53"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2371401.2371416"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0360-8"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568291"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09932-6"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984014"},{"volume-title":"Hardware and Software: Verification and Testing","author":"Bloem Roderick","key":"e_1_3_2_1_15_1","unstructured":"Roderick Bloem , Rolf Drechsler , G\u00f6rschwin Fey , Alexander Finder , Georg Hofferek , Robert K\u00f6nighofer , Jaan Raik , Urmas Repinski , and Andr\u00e9 S\u00fclflow . 2013. FoREnSiC\u2013 An Automatic Debugging Environment for C Programs . In Hardware and Software: Verification and Testing . Springer Berlin Heidelberg , Berlin, Heidelberg . 260\u2013265. isbn:978-3-642-39611-3 Roderick Bloem, Rolf Drechsler, G\u00f6rschwin Fey, Alexander Finder, Georg Hofferek, Robert K\u00f6nighofer, Jaan Raik, Urmas Repinski, and Andr\u00e9 S\u00fclflow. 2013. FoREnSiC\u2013 An Automatic Debugging Environment for C Programs. In Hardware and Software: Verification and Testing. Springer Berlin Heidelberg, Berlin, Heidelberg. 260\u2013265. isbn:978-3-642-39611-3"},{"volume-title":"Fundamental Approaches to Software Engineering","author":"Cunha Alcino","key":"e_1_3_2_1_16_1","unstructured":"Alcino Cunha , Nuno Macedo , and Tiago Guimar\u00e3es . 2014. Target Oriented Relational Model Finding . In Fundamental Approaches to Software Engineering . Springer Berlin Heidelberg , Berlin, Heidelberg . 17\u201331. isbn:978-3-642-54804-8 Alcino Cunha, Nuno Macedo, and Tiago Guimar\u00e3es. 2014. Target Oriented Relational Model Finding. In Fundamental Approaches to Software Engineering. Springer Berlin Heidelberg, Berlin, Heidelberg. 17\u201331. isbn:978-3-642-54804-8"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.15"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.66"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"volume-title":"Finding Bugs Efficiently with a SAT Solver","author":"Dolby Julian","key":"e_1_3_2_1_20_1","unstructured":"Julian Dolby , Mandana Vaziri , and Frank Tip . 2007. Finding Bugs Efficiently with a SAT Solver . In Proceedings of ESEC\/FSE. ACM Press , 195\u2013204. Julian Dolby, Mandana Vaziri, and Frank Tip. 2007. Finding Bugs Efficiently with a SAT Solver. In Proceedings of ESEC\/FSE. ACM Press, 195\u2013204."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.15"},{"key":"e_1_3_2_1_22_1","volume-title":"TACAS","author":"Gopinath Divya","year":"2011","unstructured":"Divya Gopinath , Muhammad Zubair Malik , and Sarfraz Khurshid . 2011 . Specification-Based Program Repair Using SAT. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference , TACAS 2011. 6605, Springer, 173\u2013188. Divya Gopinath, Muhammad Zubair Malik, and Sarfraz Khurshid. 2011. Specification-Based Program Repair Using SAT. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011. 6605, Springer, 173\u2013188."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples. In POPL. ACM 317\u2013330. isbn:978-1-4503-0490-0 \t\t\t\t\t  Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples. In POPL. ACM 317\u2013330. isbn:978-1-4503-0490-0","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240260"},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the 43rd ACM\/IEEE International Conference on Software Engineering ICSE 2021","author":"Brida Sim\u00f3n Guti\u00e9rrez","year":"2021","unstructured":"Sim\u00f3n Guti\u00e9rrez Brida , Germ\u00e1n Regis , Guolong Zheng , Hamid Bagheri , ThanhVu Nguyen , Nazareno Aguirre , and Marcelo Frias . 2021 . Bounded Exhaustive Search of Alloy Specification Repairs . In Proceedings of the 43rd ACM\/IEEE International Conference on Software Engineering ICSE 2021 , Virtual , May 2021. Sim\u00f3n Guti\u00e9rrez Brida, Germ\u00e1n Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo Frias. 2021. Bounded Exhaustive Search of Alloy Specification Repairs. In Proceedings of the 43rd ACM\/IEEE International Conference on Software Engineering ICSE 2021, Virtual, May 2021."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"volume-title":"Software Abstractions - Logic, Language, and Analysis","author":"Jackson Daniel","key":"e_1_3_2_1_27_1","unstructured":"Daniel Jackson . 2006. Software Abstractions - Logic, Language, and Analysis . MIT Press . isbn:978-0-262-10114-1 Daniel Jackson. 2006. Software Abstractions - Logic, Language, and Analysis. MIT Press. isbn:978-0-262-10114-1"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993544"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Barbara Jobstmann Andreas Griesmayer and Roderick Bloem. 2005. Program repair as a game. In Computer Aided Verification. 226\u2013238. \t\t\t\t\t  Barbara Jobstmann Andreas Griesmayer and Roderick Bloem. 2005. Program repair as a game. In Computer Aided Verification. 226\u2013238.","DOI":"10.1007\/11513988_23"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771798"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606626"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2010.01.049"},{"key":"e_1_3_2_1_35_1","volume-title":"Fixminer: Mining relevant fix patterns for automated program repair. Empirical Software Engineering, 1\u201345.","author":"Koyuncu Anil","year":"2020","unstructured":"Anil Koyuncu , Kui Liu , Tegawend\u00e9 F Bissyand\u00e9 , Dongsun Kim , Jacques Klein , Martin Monperrus , and Yves Le Traon . 2020 . Fixminer: Mining relevant fix patterns for automated program repair. Empirical Software Engineering, 1\u201345. Anil Koyuncu, Kui Liu, Tegawend\u00e9 F Bissyand\u00e9, Dongsun Kim, Jacques Klein, Martin Monperrus, and Yves Le Traon. 2020. Fixminer: Mining relevant fix patterns for automated program repair. Empirical Software Engineering, 1\u201345."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338935"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106309"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"e_1_3_2_1_39_1","volume-title":"Hard and Soft Constraints. In Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications","volume":"631","author":"Li Chu Min","year":"2009","unstructured":"Chu Min Li and Felip Many\u00e0 . 2009 . MaxSAT , Hard and Soft Constraints. In Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications , Vol. 185). IOS Press, 613\u2013 631 . Chu Min Li and Felip Many\u00e0. 2009. MaxSAT, Hard and Soft Constraints. In Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications, Vol. 185). IOS Press, 613\u2013631."},{"volume-title":"Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering (ICSE \u201920)","author":"Li Yi","key":"e_1_3_2_1_40_1","unstructured":"Yi Li , Shaohua Wang , and Tien N. Nguyen . 2020. DLFix: Context-Based Code Transformation Learning for Automated Program Repair . In Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering (ICSE \u201920) . Association for Computing Machinery, New York, NY, USA. 602\u2013614. isbn:9781450371216 Yi Li, Shaohua Wang, and Tien N. Nguyen. 2020. DLFix: Context-Based Code Transformation Learning for Automated Program Repair. In Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering (ICSE \u201920). Association for Computing Machinery, New York, NY, USA. 602\u2013614. isbn:9781450371216"},{"volume-title":"Automatic Patch Generation by Learning Correct Code. POPL \u201916","author":"Long Fan","key":"e_1_3_2_1_41_1","unstructured":"Fan Long and Martin Rinard . 2016. Automatic Patch Generation by Learning Correct Code. POPL \u201916 . Association for Computing Machinery , New York, NY, USA . 298\u2013312. isbn:9781450335492 Fan Long and Martin Rinard. 2016. Automatic Patch Generation by Learning Correct Code. POPL \u201916. Association for Computing Machinery, New York, NY, USA. 298\u2013312. isbn:9781450335492"},{"key":"e_1_3_2_1_42_1","volume-title":"ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. 12071","author":"Macedo Nuno","year":"2020","unstructured":"Nuno Macedo , Alcino Cunha , Jos\u00e9 Pereira , Renato Carvalho , Ricardo Silva , Ana C. R. Paiva , Miguel Sozinho Ramalho , and Daniel Castro Silva . 2020 . Experiences on Teaching Alloy with an Automated Assessment Platform. In Rigorous State-Based Methods - 7th International Conference , ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. 12071 , Springer, 61\u201377. Nuno Macedo, Alcino Cunha, Jos\u00e9 Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, and Daniel Castro Silva. 2020. Experiences on Teaching Alloy with an Automated Assessment Platform. In Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. 12071, Springer, 61\u201377."},{"key":"e_1_3_2_1_43_1","volume-title":"ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings (Lecture Notes in Computer Science","volume":"317","author":"Maldonado-Lopez Ferney A.","year":"2014","unstructured":"Ferney A. Maldonado-Lopez , Jaime Chavarriaga , and Yezid Donoso . 2014 . Detecting Network Policy Conflicts Using Alloy. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference , ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings (Lecture Notes in Computer Science , Vol. 8477). Springer, 314\u2013 317 . Ferney A. Maldonado-Lopez, Jaime Chavarriaga, and Yezid Donoso. 2014. Detecting Network Policy Conflicts Using Alloy. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8477). Springer, 314\u2013317."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3275534"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989787"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.63"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_48_1","volume-title":"DeepDelta: Learning to Repair Compilation Errors. ESEC\/FSE","author":"Mesbah Ali","year":"2019","unstructured":"Ali Mesbah , Andrew Rice , Emily Johnston , Nick Glorioso , and Edward Aftandilian . 2019. DeepDelta: Learning to Repair Compilation Errors. ESEC\/FSE 2019 . Association for Computing Machinery , New York, NY, USA . 925\u2013936. isbn:9781450355728 Ali Mesbah, Andrew Rice, Emily Johnston, Nick Glorioso, and Edward Aftandilian. 2019. DeepDelta: Learning to Repair Compilation Errors. ESEC\/FSE 2019. Association for Computing Machinery, New York, NY, USA. 925\u2013936. isbn:9781450355728"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884853"},{"volume-title":"Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201914)","author":"Joseph","key":"e_1_3_2_1_50_1","unstructured":"Joseph P. Near and Daniel Jackson. 2014. Derailer: Interactive Security Analysis for Web Applications . In Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201914) . ACM, New York, NY, USA. 587\u2013598. isbn:978-1-4503-3013-8 Joseph P. Near and Daniel Jackson. 2014. Derailer: Interactive Security Analysis for Web Applications. In Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201914). ACM, New York, NY, USA. 587\u2013598. isbn:978-1-4503-3013-8"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 38th International Conference on Software Engineering, ICSE 2016","author":"Joseph","year":"2016","unstructured":"Joseph P. Near and Daniel Jackson. 2016. Finding security bugs in web applications using a catalog of access control patterns . In Proceedings of the 38th International Conference on Software Engineering, ICSE 2016 , Austin, TX, USA , May 14-22, 2016 . 947\u2013958. Joseph P. Near and Daniel Jackson. 2016. Finding security bugs in web applications using a catalog of access control patterns. In Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016. 947\u2013958."},{"key":"e_1_3_2_1_52_1","volume-title":"The Margrave Tool for Firewall Analysis. In Uncovering the Secrets of System Administration: Proceedings of the 24th Large Installation System Administration Conference, LISA 2010","author":"Nelson Timothy","year":"2010","unstructured":"Timothy Nelson , Christopher Barratt , Daniel J. Dougherty , Kathi Fisler , and Shriram Krishnamurthi . 2010 . The Margrave Tool for Firewall Analysis. In Uncovering the Secrets of System Administration: Proceedings of the 24th Large Installation System Administration Conference, LISA 2010 , San Jose, CA, USA , November 7-12, 2010. USENIX Association. Timothy Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2010. The Margrave Tool for Firewall Analysis. In Uncovering the Secrets of System Administration: Proceedings of the 24th Large Installation System Administration Conference, LISA 2010, San Jose, CA, USA, November 7-12, 2010. USENIX Association."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_17"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001429"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSNT.2011.141"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.3390\/app11010303"},{"key":"e_1_3_2_1_58_1","volume-title":"Field-exhaustive Testing. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE","author":"Ponzio Pablo","year":"2016","unstructured":"Pablo Ponzio , Nazareno Aguirre , Marcelo F. Frias , and Willem Visser . 2016 . Field-exhaustive Testing. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, New York, NY, USA. 908\u2013919. isbn:978-1-4503-4218-6 Pablo Ponzio, Nazareno Aguirre, Marcelo F. Frias, and Willem Visser. 2016. Field-exhaustive Testing. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, New York, NY, USA. 908\u2013919. isbn:978-1-4503-4218-6"},{"volume-title":"Security Analysis of Bytecode Interpreters Using Alloy","author":"Reynolds Mark Clifford","key":"e_1_3_2_1_59_1","unstructured":"Mark Clifford Reynolds . 2012. Security Analysis of Bytecode Interpreters Using Alloy . Boston University . Boston, MA, USA. isbn:978-1-267-52285-6 Mark Clifford Reynolds. 2012. Security Analysis of Bytecode Interpreters Using Alloy. Boston University. Boston, MA, USA. isbn:978-1-267-52285-6"},{"volume-title":"Proceedings of the International Symposium on Software Testing and Analysis (ISSTA). 23\u201333","author":"Rosner N.","key":"e_1_3_2_1_60_1","unstructured":"N. Rosner , Juan Galeotti , Santiago Bermudez , Guido Marucci Blas , Santiago Perez De Rosso , Lucas Pizzagalli , Luciano Zemin , and Marcelo F. Frias . 2013. Parallel Bounded Analysis in Code with Rich Invariants by Refinement of Field Bounds . In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA). 23\u201333 . N. Rosner, Juan Galeotti, Santiago Bermudez, Guido Marucci Blas, Santiago Perez De Rosso, Lucas Pizzagalli, Luciano Zemin, and Marcelo F. Frias. 2013. Parallel Bounded Analysis in Code with Rich Invariants by Refinement of Field Bounds. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA). 23\u201333."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2491711"},{"key":"e_1_3_2_1_62_1","volume-title":"ECSA 2016, Copenhagen, Denmark, November 28 - December 2, 2016, Proceedings. 274\u2013290","author":"Schmerl Bradley R.","year":"2016","unstructured":"Bradley R. Schmerl , Jeff Gennari , Alireza Sadeghi , Hamid Bagheri , Sam Malek , Javier C\u00e1mara , and David Garlan . 2016 . Architecture Modeling and Analysis of Security in Android Systems. In Software Architecture - 10th European Conference , ECSA 2016, Copenhagen, Denmark, November 28 - December 2, 2016, Proceedings. 274\u2013290 . Bradley R. Schmerl, Jeff Gennari, Alireza Sadeghi, Hamid Bagheri, Sam Malek, Javier C\u00e1mara, and David Garlan. 2016. Architecture Modeling and Analysis of Security in Android Systems. In Software Architecture - 10th European Conference, ECSA 2016, Copenhagen, Denmark, November 28 - December 2, 2016, Proceedings. 274\u2013290."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1512762.1512764"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Rishabh Singh Sumit Gulwani and Armando Solar-Lezama. 2013. Automated feedback generation for introductory programming assignments. In PLDI. 15\u201326. \t\t\t\t\t  Rishabh Singh Sumit Gulwani and Armando Solar-Lezama. 2013. Automated feedback generation for introductory programming assignments. In PLDI. 15\u201326.","DOI":"10.1145\/2499370.2462195"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_1_66_1","volume-title":"Foster","author":"Srivastava Saurabh","year":"2010","unstructured":"Saurabh Srivastava , Sumit Gulwani , and Jeffrey S . Foster . 2010 . From program verification to program synthesis. In POPL. ACM , 313\u2013326. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. In POPL. ACM, 313\u2013326."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_3_2_1_68_1","volume-title":"42nd International Conference on Software Engineering","author":"Stevens Clay","year":"2020","unstructured":"Clay Stevens and Hamid Bagheri . 2020 . Reducing run-time adaptation space via analysis of possible utility bounds. In ICSE \u201920 : 42nd International Conference on Software Engineering , Seoul, South Korea, 27 June - 19 July, 2020. ACM, 1522\u20131534. Clay Stevens and Hamid Bagheri. 2020. Reducing run-time adaptation space via analysis of possible utility bounds. In ICSE \u201920: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June - 19 July, 2020. ACM, 1522\u20131534."},{"key":"e_1_3_2_1_69_1","volume-title":"AUnit: A Test Automation Tool for Alloy. In 11th IEEE International Conference on Software Testing, Verification and Validation, ICST 2018","author":"Sullivan Allison","year":"2018","unstructured":"Allison Sullivan , Kaiyuan Wang , and Sarfraz Khurshid . 2018 . AUnit: A Test Automation Tool for Alloy. In 11th IEEE International Conference on Software Testing, Verification and Validation, ICST 2018 , V\u00e4ster\u00e5s, Sweden , April 9-13, 2018. IEEE Computer Society, 398\u2013403. Allison Sullivan, Kaiyuan Wang, and Sarfraz Khurshid. 2018. AUnit: A Test Automation Tool for Alloy. In 11th IEEE International Conference on Software Testing, Verification and Validation, ICST 2018, V\u00e4ster\u00e5s, Sweden, April 9-13, 2018. IEEE Computer Society, 398\u2013403."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025115.1025215"},{"volume-title":"Automating Modular Program Verification by Refining Specifications","author":"Taghdiri Mana","key":"e_1_3_2_1_71_1","unstructured":"Mana Taghdiri . 2007. Automating Modular Program Verification by Refining Specifications . Massachusetts Institute of Technology . Mana Taghdiri. 2007. Automating Modular Program Verification by Refining Specifications. Massachusetts Institute of Technology."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000291"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238162"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00049"},{"key":"e_1_3_2_1_75_1","volume-title":"Fault Localization for Declarative Models in Alloy. In 31st IEEE International Symposium on Software Reliability Engineering, ISSRE 2020","author":"Wang Kaiyuan","year":"2020","unstructured":"Kaiyuan Wang , Allison Sullivan , Darko Marinov , and Sarfraz Khurshid . 2020 . Fault Localization for Declarative Models in Alloy. In 31st IEEE International Symposium on Software Reliability Engineering, ISSRE 2020 , Coimbra, Portugal , October 12-15, 2020. IEEE, 391\u2013402. Kaiyuan Wang, Allison Sullivan, Darko Marinov, and Sarfraz Khurshid. 2020. Fault Localization for Declarative Models in Alloy. In 31st IEEE International Symposium on Software Reliability Engineering, ISSRE 2020, Coimbra, Portugal, October 12-15, 2020. IEEE, 391\u2013402."},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282517.3282528"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00065"}],"event":{"name":"ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Virtual South Korea","acronym":"ISSTA '22"},"container-title":["Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534369","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3533767.3534369","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:40Z","timestamp":1750272220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534369"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":77,"alternative-id":["10.1145\/3533767.3534369","10.1145\/3533767"],"URL":"https:\/\/doi.org\/10.1145\/3533767.3534369","relation":{},"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"2022-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}