{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:51Z","timestamp":1750220091146,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["1563920"],"award-info":[{"award-number":["1563920"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,18]]},"DOI":"10.1145\/3524482.3527650","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"46-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Counterexample-guided inductive repair of reactive contracts"],"prefix":"10.1145","author":[{"given":"Soha","family":"Hussein","sequence":"first","affiliation":[{"name":"University of Minnesota"}]},{"given":"Sanjai","family":"Rayadurgam","sequence":"additional","affiliation":[{"name":"University of Minnesota"}]},{"given":"Stephen","family":"McCamant","sequence":"additional","affiliation":[{"name":"University of Minnesota"}]},{"given":"Vaibhav","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of Minnesota"}]},{"given":"Mats","family":"Heimdahl","sequence":"additional","affiliation":[{"name":"University of Minnesota"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"volume-title":"Retrieved","year":"2022","key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. ContractDR GitHub Repository . Retrieved March 29, 2022 from https:\/\/github.com\/sohah\/ContractDR [n.d.]. ContractDR GitHub Repository. Retrieved March 29, 2022 from https:\/\/github.com\/sohah\/ContractDR"},{"volume-title":"jpf-symbc. Retrieved","year":"2022","key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. jpf-symbc. Retrieved March 29, 2022 from https:\/\/github.com\/SymbolicPathFinder\/jpf-symbc [n.d.]. jpf-symbc. Retrieved March 29, 2022 from https:\/\/github.com\/SymbolicPathFinder\/jpf-symbc"},{"volume-title":"d.]. Lustre. Retrieved","year":"2022","key":"e_1_3_2_1_3_1","unstructured":"[n. d.]. Lustre. Retrieved March 29, 2022 from http:\/\/www-verimag.imag.fr\/The-Lustre-Programming-Language-and [n. d.]. Lustre. Retrieved March 29, 2022 from http:\/\/www-verimag.imag.fr\/The-Lustre-Programming-Language-and"},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. Z3. Retrieved March 29 2022 from https:\/\/rise4fun.com\/z3\/tutorial  [n.d.]. Z3. Retrieved March 29 2022 from https:\/\/rise4fun.com\/z3\/tutorial"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_1"},{"key":"e_1_3_2_1_6_1","volume-title":"FMCAD 2013 (aug","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Salar Moarref , and Ufuk Topcu . 2013 . Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications. 2013 Formal Methods in Computer-Aided Design , FMCAD 2013 (aug 2013), 26--33. arXiv:1308.4113 https:\/\/arxiv.org\/abs\/1308.4113v1 Rajeev Alur, Salar Moarref, and Ufuk Topcu. 2013. Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications. 2013 Formal Methods in Computer-Aided Design, FMCAD 2013 (aug 2013), 26--33. arXiv:1308.4113 https:\/\/arxiv.org\/abs\/1308.4113v1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/HCMDSS-MDPNP.2007.36"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873653"},{"key":"e_1_3_2_1_9_1","volume-title":"CoRR abs\/1611.0","author":"Cavezza Davide G.","year":"2016","unstructured":"Davide G. Cavezza . 2016. Interpolation-Based GR(1) Assumptions Refinement . CoRR abs\/1611.0 ( 2016 ). http:\/\/arxiv.org\/abs\/1611.07803 Davide G. Cavezza. 2016. Interpolation-Based GR(1) Assumptions Refinement. CoRR abs\/1611.0 (2016). http:\/\/arxiv.org\/abs\/1611.07803"},{"key":"e_1_3_2_1_10_1","unstructured":"Hoang Duong Thien Nguyen and Satish Chandra. 2013. SemFix : Program Repair via Semantic Analysis. In ICSE. 772--781. https:\/\/compsec.comp.nus.edu.sg\/papers\/ICSE13-SEMFIX.pdf  Hoang Duong Thien Nguyen and Satish Chandra. 2013. SemFix : Program Repair via Semantic Analysis. In ICSE. 772--781. https:\/\/compsec.comp.nus.edu.sg\/papers\/ICSE13-SEMFIX.pdf"},{"key":"e_1_3_2_1_11_1","unstructured":"Michael D Ernst and Contributors. 2020. {Daikon} User Manual (version 5.8.4 ed.). https:\/\/plse.cs.washington.edu\/daikon\/download\/doc\/daikon.pdf  Michael D Ernst and Contributors. 2020. {Daikon} User Manual (version 5.8.4 ed.). https:\/\/plse.cs.washington.edu\/daikon\/download\/doc\/daikon.pdf"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2007.01.015"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_3"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264600"},{"key":"e_1_3_2_1_17_1","volume-title":"Counterexample Guided Inductive Repair of Reactive Contracts. In 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1190--1192","author":"Hussein Soha","year":"2021","unstructured":"Soha Hussein , Vaibhav Sharma , Stephen McCamant , Sanjai Rayadurgam , and Mats Heimdahl . 2021 . Counterexample Guided Inductive Repair of Reactive Contracts. In 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1190--1192 . Soha Hussein, Vaibhav Sharma, Stephen McCamant, Sanjai Rayadurgam, and Mats Heimdahl. 2021. Counterexample Guided Inductive Repair of Reactive Contracts. In 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1190--1192."},{"key":"e_1_3_2_1_18_1","unstructured":"Soha Hussein Vaibhav Sharma Michael W Whalen Stephen McCamant and Willem Visser. [n. d.]. JavaRanger. https:\/\/github.com\/vaibhavbsharma\/java-ranger  Soha Hussein Vaibhav Sharma Michael W Whalen Stephen McCamant and Willem Visser. [n. d.]. JavaRanger. https:\/\/github.com\/vaibhavbsharma\/java-ranger"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106240"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106309"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786811"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00106"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2948705"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180247"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155662"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93578"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering","author":"Corina","key":"e_1_3_2_1_33_1","unstructured":"Corina S. P\u0103s\u0103reanu and Neha Rungta. 2010. Symbolic PathFinder: Symbolic Execution of Java Bytecode . In Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering ( Antwerp, Belgium) (ASE '10). Association for Computing Machinery, New York, NY, USA, 179--180. Corina S. P\u0103s\u0103reanu and Neha Rungta. 2010. Symbolic PathFinder: Symbolic Execution of Java Bytecode. In Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering (Antwerp, Belgium) (ASE '10). Association for Computing Machinery, New York, NY, USA, 179--180."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126504"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327757.3327873"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542501"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-012-0223-4"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468596"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207115"},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems (FMICS'07)","author":"Whalen Michael","year":"2007","unstructured":"Michael Whalen , Darren Cofer , Steven Miller , Bruce H Krogh , and Walter Storm . 2007 . Integration of Formal Analysis into a Model-Based Software Development Process . In Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems (FMICS'07) . Springer-Verlag, Berlin, Heidelberg, 68--84. Michael Whalen, Darren Cofer, Steven Miller, Bruce H Krogh, and Walter Storm. 2007. Integration of Formal Analysis into a Model-Based Software Development Process. In Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems (FMICS'07). Springer-Verlag, Berlin, Heidelberg, 68--84."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610389"}],"event":{"name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Pittsburgh Pennsylvania","acronym":"FormaliSE '22"},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527650","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527650","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:51Z","timestamp":1750183791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527650"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":43,"alternative-id":["10.1145\/3524482.3527650","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527650","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}