{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T23:25:05Z","timestamp":1781565905547,"version":"3.54.5"},"reference-count":97,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T00:00:00Z","timestamp":1778630400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"crossref","award":["Grant No. 1954\/23, SPECTACKLE"],"award-info":[{"award-number":["Grant No. 1954\/23, SPECTACKLE"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite significant research progress in the past decades, reactive synthesis is still in early stage of use. Previous studies found that the lack of development methods for reactive synthesis specifications is one barrier to its wider adoption. In this article, we adapt two development methods, an incremental method and a modular method, to the context of reactive synthesis specifications. The methods are based on existing software development methods on the one hand and studies about reactive synthesis on the other hand. Then, we report on an exploratory case study in which participants developed specifications using the two methods. We evaluated the methods using a mixed-method analysis that combines grounded theory analysis of Slack communication with participants, quantitative exploratory data analysis of the synthesis IDE usage logs, and qualitative independent expert review of the final specifications. Our findings show clear benefits of modular specification development in terms of ease of planning, synthesis time, fewer unrealizability issues, and faster debugging. However, the incremental development method was more natural and easy to use, and specifications developed incrementally were also easier to validate during the development process.<\/jats:p>","DOI":"10.1145\/3767159","type":"journal-article","created":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T22:22:26Z","timestamp":1757629346000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Exploring Development Methods for Reactive Synthesis Specifications"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7290-2789","authenticated-orcid":false,"given":"Dor","family":"Ma\u2019ayan","sequence":"first","affiliation":[{"name":"School of Computer Science and AI, Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4022-5349","authenticated-orcid":false,"given":"Shahar","family":"Maoz","sequence":"additional","affiliation":[{"name":"School of Computer Science and AI, Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3610-3920","authenticated-orcid":false,"given":"Jan Oliver","family":"Ringert","sequence":"additional","affiliation":[{"name":"Bauhaus University Weimar, Weimar, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,5,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-017-9665-6"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00070"},{"key":"e_1_3_2_4_2","first-page":"729","volume-title":"Formal Aspects of Computing","volume":"33","author":"Amram G.","year":"2021","unstructured":"G. Amram, S. Maoz, and O. Pistiner. 2021. GR(1)*: GR(1) specifications extended with existential guarantees. Formal Aspects of Computing 33, 4\u20135 (2021), 729\u2013761."},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/ICRE.1996.491438","volume-title":"Proceedings of the 2nd International Conference on Requirements Engineering (ICRE \u201996)","author":"Ant\u00f3n A. I.","year":"1996","unstructured":"A. I. Ant\u00f3n. 1996. Goal-based requirements analysis. In Proceedings of the 2nd International Conference on Requirements Engineering (ICRE \u201996). IEEE Computer Society, Colorado Springs, Colorado, 136\u2013144."},{"issue":"5","key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.5381\/jot.2009.8.5.c5","article-title":"An overview of feature-oriented software development","volume":"8","author":"Apel S.","year":"2009","unstructured":"S. Apel and C. K\u00e4stner. 2009. An overview of feature-oriented software development. The Journal of Object Technology 8, 5 (2009), 49\u201384.","journal-title":"The Journal of Object Technology"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2366.001.0001"},{"key":"e_1_3_2_8_2","unstructured":"K. Beck M. Beedle A. Van Bennekum A. Cockburn W. Cunningham M. Fowler J. Grenning J. Highsmith A. Hunt R. Jeffries et al. 2001. Manifesto for agile software development. Retrieved form https:\/\/agilemanifesto.org\/"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/318762"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/376"},{"key":"e_1_3_2_11_2","first-page":"263","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV \u201907)","volume":"4590","author":"Bloem R.","unstructured":"R. Bloem, R. Cavada, I. Pill, M. Roveri, and A. Tchaltsev. 2007. RAT: A tool for the formal analysis of requirements. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV \u201907). W. Damm and H. Hermanns (Eds.), Lecture Notes in Computer Science, Vol. 4590, Springer, 263\u2013267."},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"Bloem R.","year":"2010","unstructured":"R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. K\u00f6nighofer, M. Roveri, V. Schuppan, and R. Seeber. 2010. RATSY\u2014A new requirements analysis tool with synthesis. In Computer Aided Verification. T. Touili, B. Cook, and P. Jackson (Eds.), Springer, Berlin, 425\u2013429."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"issue":"5","key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/2.59","article-title":"A spiral model of software development and enhancement","volume":"21","author":"Boehm B. W.","year":"1988","unstructured":"B. W. Boehm. 1988. A spiral model of software development and enhancement. Computer 21, 5 (1988), 61\u201372.","journal-title":"Computer"},{"key":"e_1_3_2_15_2","volume-title":"Transforming Qualitative Information: Thematic Analysis and Code Development","author":"Boyatzis R. E.","year":"1998","unstructured":"R. E. Boyatzis. 1998. Transforming Qualitative Information: Thematic Analysis and Code Development. Sage."},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"1347","DOI":"10.1109\/ICSE.2013.6606714","volume-title":"Proceedings of the 2013 International Conference on Software Engineering (ICSE \u201913)","author":"Braberman V.","year":"2013","unstructured":"V. Braberman, N. D\u2019Ippolito, N. Piterman, D. Sykes, and S. Uchitel. 2013. Controller synthesis: From modelling to enactment. In Proceedings of the 2013 International Conference on Software Engineering (ICSE \u201913). IEEE Press, 1347\u20131350."},{"key":"e_1_3_2_17_2","first-page":"303","volume-title":"Conference on Object-Oriented Programming Systems, Languages, and Applications\/European Conference on Object-Oriented Programming (OOPSLA\/ECOOP \u201990)","author":"Bracha G.","unstructured":"G. Bracha and W. R. Cook. 1990. Mixin-based inheritance. In Conference on Object-Oriented Programming Systems, Languages, and Applications\/European Conference on Object-Oriented Programming (OOPSLA\/ECOOP \u201990). A. Yonezawa (Ed.), ACM, 303\u2013311."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"D. G. Cavezza D. Alrajeh and A. Gy\u00f6rgy. Minimal assumptions refinement for realizable specifications. In FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering Seoul Republic of Korea July 13 2020. K. Bae D. Bianculli S. Gnesi and N. Plat (Eds.) ACM 66\u201376. DOI: 10.1145\/3372020.3391557","DOI":"10.1145\/3372020.3391557"},{"key":"e_1_3_2_19_2","first-page":"171","volume-title":"Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201917)","author":"\u00c7elik A.","unstructured":"A. \u00c7elik, K. Palmskog, and M. Gligoric. 2017. iCoq: Regression proof selection for large-scale verification projects. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201917). G. Rosu, M. D. Penta, and T. N. Nguyen (Eds.), IEEE Computer Society, 171\u2013182."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183493"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV \u201902)","volume":"2404","author":"Cimatti A.","unstructured":"A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV 2: An OpenSource tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV \u201902). E. Brinksma and K. G. Larsen (Eds.), Lecture Notes in Computer Science, Vol. 2404, Springer, 359\u2013364."},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Cimatti A.","year":"2008","unstructured":"A. Cimatti, M. Roveri, V. Schuppan, and A. Tchaltsev. 2008. Diagnostic information for realizability. In Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation, Springer, 52\u201367."},{"key":"e_1_3_2_23_2","first-page":"331","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference (TACAS \u201903), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS \u201903)Lecture Notes in Computer Science","volume":"2619","author":"Cobleigh J. M.","year":"2003","unstructured":"J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. 2003. Learning assumptions for compositional verification. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference (TACAS \u201903), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS \u201903). H. Garavel and J. Hatcliff (Eds.), Lecture Notes in Computer Science, Vol. 2619, Springer, 331\u2013346."},{"key":"e_1_3_2_24_2","volume-title":"Basics of Qualitative Research: Techniques and Procedures for Developing Grounded Theory","author":"Corbin J.","year":"2014","unstructured":"J. Corbin and A. Strauss. 2014. Basics of Qualitative Research: Techniques and Procedures for Developing Grounded Theory. Sage Publications."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66197-1_11"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(93)90021-G"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/239098.239131"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.4324\/9781315129945"},{"key":"e_1_3_2_29_2","volume-title":"Software Verification and Validation: Realistic Project Approaches","author":"Deutsch M. S.","year":"1981","unstructured":"M. S. Deutsch. 1981. Software Verification and Validation: Realistic Project Approaches. Prentice Hall PTR."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985823"},{"key":"e_1_3_2_31_2","first-page":"77","volume-title":"Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering","author":"D\u2019Ippolito N.","year":"2010","unstructured":"N. D\u2019Ippolito, V. A. Braberman, N. Piterman, and S. Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering. G. Roman and A. van der Hoek (Eds.), ACM, 77\u201386."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_33_2","first-page":"333","volume-title":"Computer Aided Verification","author":"Ehlers R.","year":"2016","unstructured":"R. Ehlers and V. Raman. 2016. Slugs: Extensible GR(1) Synthesis. In Computer Aided Verification. S. Chaudhuri and A. Farzan (Eds.), Springer International Publishing, 333\u2013339."},{"key":"e_1_3_2_34_2","first-page":"1030","volume-title":"Proceedings of the 2016 IEEE Conference on Control Applications (CCA \u201916)","author":"Filippidis I.","unstructured":"I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay, and R. M. Murray. 2016. Control design for hybrid systems with TuLiP: The temporal logic planning toolbox. In Proceedings of the 2016 IEEE Conference on Control Applications (CCA \u201916), 1030\u20131041."},{"key":"e_1_3_2_35_2","first-page":"1988","volume-title":"Proceedings of the 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems","author":"Finucane C.","unstructured":"C. Finucane, G. Jing, and H. Kress-Gazit. 2010. LTLMoP: Experimenting with language, temporal logic and robot control. In Proceedings of the 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems, 1988\u20131993."},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"4th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC \u201908)Lecture Notes in Computer Science","volume":"5394","author":"Fisman D.","unstructured":"D. Fisman, O. Kupferman, S. Sheinvald-Faragy, and M. Y. Vardi. 2008. A framework for inherent vacuity. In 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC \u201908). H. Chockler and A. J. Hu (Eds.), Lecture Notes in Computer Science, Vol. 5394, Springer, 7\u201322."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03160222"},{"key":"e_1_3_2_38_2","first-page":"1","volume-title":"Proceedings of the 46th IEEE\/ACM International Conference on Software Engineering (ICSE \u201924)","author":"Gorenstein A.","year":"2024","unstructured":"A. Gorenstein, S. Maoz, and J. O. Ringert. 2024. Kind controllers and fast heuristics for non-well-separated GR(1) specifications. In Proceedings of the 46th IEEE\/ACM International Conference on Software Engineering (ICSE \u201924). ACM, 1\u201312."},{"issue":"10","key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"3808","DOI":"10.1109\/TSE.2021.3106280","article-title":"Socio-technical grounded theory for software engineering","volume":"48","author":"Hoda R.","year":"2022","unstructured":"R. Hoda. 2022. Socio-technical grounded theory for software engineering. IEEE Transactions on Software Engineering 48, 10 (2022), 3808\u20133832.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","article-title":"Alloy: A lightweight object modelling notation","volume":"11","author":"Jackson D.","year":"2002","unstructured":"D. Jackson. 2002. Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11, 2 (2002), 256\u2013290.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/225014.225041"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/590564.590577"},{"key":"e_1_3_2_43_2","first-page":"15","volume-title":"Proceedings of the 17th International Conference on Software Engineering","author":"Jackson M.","year":"1995","unstructured":"M. Jackson and P. Zave. 1995. Deriving specifications from requirements: An example. In Proceedings of the 17th International Conference on Software Engineering, 15\u201324."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027796"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19583-9_16"},{"issue":"5","key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1007\/s10009-011-0221-y","article-title":"Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies","volume":"15","author":"K\u00f6nighofer R.","year":"2013","unstructured":"R. K\u00f6nighofer, G. Hofferek, and R. Bloem. 2013. Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies. International Journal on Software Tools for Technology Transfer 15, 5 (2013), 563\u2013583.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"e_1_3_2_47_2","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","article-title":"Temporal-logic-based reactive mission and motion planning","volume":"25","author":"Kress-Gazit H.","year":"2009","unstructured":"H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. 2009. Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics 25, 6 (2009), 1370\u20131381.","journal-title":"IEEE Transactions on Robotics"},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-030-30942-8_1","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"Krishnamurthi S.","year":"2019","unstructured":"S. Krishnamurthi and T. Nelson. 2019. The human in formal methods. In Formal Methods \u2013 The Next 30 Years. M. H. ter Beek, A. McIver, and J. N. Oliveira (Eds.), Springer International Publishing, 3\u201310."},{"key":"e_1_3_2_49_2","first-page":"37","volume-title":"Proceedings of the 17th International Conference on Concurrency Theory (CONCUR \u201906)Lecture Notes in Computer Science","author":"Kupferman O.","year":"2006","unstructured":"O. Kupferman. 2006. Sanity checks in formal verification. In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR \u201906). C. Baier and H. Hermanns (Eds.), Lecture Notes in Computer Science, Vol. 4137, Springer, 37\u201351."},{"key":"e_1_3_2_50_2","first-page":"312","volume-title":"Proceedings of the 6th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16)","volume":"6355","author":"Kupferman O.","year":"2010","unstructured":"O. Kupferman and M. Y. Vardi. 2010. Synthesis of trigger properties. In Proceedings of the 6th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16). E. M. Clarke and A. Voronkov (Eds.), Lecture Notes in Computer Science, Vol. 6355, Springer, 312\u2013331."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106240"},{"key":"e_1_3_2_52_2","first-page":"602","volume-title":"Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201916)","author":"Legunsen O.","unstructured":"O. Legunsen, W. U. Hassan, X. Xu, G. Rosu, and D. Marinov. 2016. How good are the specs? A study of the bug-finding effectiveness of existing java API specifications. In Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201916). D. Lo, S. Apel, and S. Khurshid (Eds.), ACM, 602\u2013613."},{"key":"e_1_3_2_53_2","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1109\/ICST.2019.00037","volume-title":"Proceedings of the 12th IEEE Conference on Software Testing, Validation and Verification (ICST \u201919)","author":"Legunsen O.","year":"2019","unstructured":"O. Legunsen, Y. Zhang, M. Hadzi-Tanovic, G. Rosu, and D. Marinov. 2019. Techniques for evolution-aware runtime verification. In Proceedings of the 12th IEEE Conference on Software Testing, Validation and Verification (ICST \u201919). IEEE, 300\u2013311."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00071"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-NIER58687.2023.00009"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1145\/3550355.3552425","volume-title":"Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems (MODELS \u201922)","author":"Ma\u2019ayan D.","year":"2022","unstructured":"D. Ma\u2019ayan, S. Maoz, and R. Rozi. 2022. Validating the correctness of reactive systems specifications through systematic exploration. In Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems (MODELS \u201922). E. Syriani, H. A. Sahraoui, N. Bencomo, and M. Wimmer (Eds.), ACM, 132\u2013142."},{"key":"e_1_3_2_57_2","first-page":"229","volume-title":"Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201919), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS \u201919)Lecture Notes in Computer Science","volume":"11428","author":"Majumdar R.","year":"2019","unstructured":"R. Majumdar, N. Piterman, and A. Schmuck. 2019. Environmentally-friendly GR(1) synthesis. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201919), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS \u201919). T. Vojnar and L. Zhang (Eds.), Lecture Notes in Computer Science, Vol. 11428, Springer, 229\u2013246."},{"key":"e_1_3_2_58_2","first-page":"4192","volume-title":"Proceedings of the 2016 IEEE International Conference on Robotics and Automation (ICRA)","author":"Maniatopoulos S.","year":"2016","unstructured":"S. Maniatopoulos, P. Schillinger, V. Pong, D. C. Conner, and H. Kress-Gazit. 2016. Reactive high-level behavior synthesis for an atlas humanoid robot. In Proceedings of the 2016 IEEE International Conference on Robotics and Automation (ICRA), 4192\u20134199."},{"issue":"1","key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1214\/aoms\/1177730491","article-title":"On a test of whether one of two random variables is stochastically larger than the other","volume":"18","author":"Mann H. B.","year":"1947","unstructured":"H. B. Mann and D. R. Whitney. 1947. On a test of whether one of two random variables is stochastically larger than the other. The Annals of Mathematical Statistics 18, 1 (1947), 50\u201360.","journal-title":"The Annals of Mathematical Statistics"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE58978.2023.00013"},{"key":"e_1_3_2_61_2","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1145\/2786805.2786824","volume-title":"Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE \u201915)","author":"Maoz S.","year":"2015","unstructured":"S. Maoz and J. O. Ringert. 2015. GR(1) synthesis for LTL specification patterns. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE \u201915). ACM, New York, NY, 96\u2013106."},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950300"},{"key":"e_1_3_2_63_2","first-page":"320","volume-title":"Proceedings of the 2021 IEEE\/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)","author":"Maoz S.","year":"2021","unstructured":"S. Maoz and J. O. Ringert. 2021. Reactive synthesis with spectra: A tutorial. In Proceedings of the 2021 IEEE\/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 320\u2013321."},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-021-00868-z"},{"key":"e_1_3_2_65_2","first-page":"1016","volume-title":"Proceedings of the 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE)","author":"Maoz S.","year":"2019","unstructured":"S. Maoz, J. O. Ringert, and R. Shalom. 2019. Symbolic repairs for GR(1) specifications. In Proceedings of the 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE), 1016\u20131026."},{"key":"e_1_3_2_66_2","first-page":"242","volume-title":"Proceedings of the 35th International Conference on Software Engineering (ICSE \u201913)","author":"Maoz S.","unstructured":"S. Maoz and Y. Sa\u2019ar. Counter play-out: Executing unrealizable scenario-based specifications. In Proceedings of the 35th International Conference on Software Engineering (ICSE \u201913). D. Notkin, B. H. C. Cheng, and K. Pohl (Eds.), IEEE Computer Society, 242\u2013251."},{"key":"e_1_3_2_67_2","first-page":"99","volume-title":"Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920)","author":"Maoz S.","year":"2020","unstructured":"S. Maoz and R. Shalom. 2020. Inherent vacuity for GR(1) specifications. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920). ACM, New York, NY, 99\u2013110."},{"key":"e_1_3_2_68_2","first-page":"25","volume-title":"Proceedings of the 43rd International Conference on Software Engineering (ICSE)","author":"Maoz S.","year":"2021","unstructured":"S. Maoz and R. Shalom. 2021. Unrealizable cores for reactive systems specifications. In Proceedings of the 43rd International Conference on Software Engineering (ICSE), IEEE Press, 25\u201336."},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2945329"},{"issue":"5","key":"e_1_3_2_70_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MS.1987.231413","article-title":"Cleanroom software engineering","volume":"4","author":"Mills H. D.","year":"1987","unstructured":"H. D. Mills, M. G. Dyer, and R. C. Linger. 1987. Cleanroom software engineering. IEEE Software 4, 5 (1987), 19\u201325.","journal-title":"IEEE Software"},{"key":"e_1_3_2_71_2","volume-title":"Software Reliability\u2014Principles and Practices","author":"Myers G. J.","year":"1976","unstructured":"G. J. Myers. 1976. Software Reliability\u2014Principles and Practices. Wiley."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/581339.581450"},{"issue":"3","key":"e_1_3_2_73_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1109\/2.910904","article-title":"Weaving together requirements and architectures","volume":"34","author":"Nuseibeh B.","year":"2001","unstructured":"B. Nuseibeh. 2001. Weaving together requirements and architectures. Computer 34, 3 (2001), 115\u2013117.","journal-title":"Computer"},{"key":"e_1_3_2_74_2","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/3209108.3209109","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201918)","author":"O\u2019Hearn P. W.","year":"2018","unstructured":"P. W. O\u2019Hearn. 2018. Continuous reasoning: Scaling the impact of formal methods. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201918). A. Dawar and E. Gr\u00e4del (Eds.), ACM, 13\u201325."},{"key":"e_1_3_2_75_2","first-page":"821","volume-title":"Proceedings of the 43rd Design Automation Conference (DAC \u201906)","author":"Pill I.","unstructured":"I. Pill, S. Semprini, R. Cavada, M. Roveri, R. Bloem, and A. Cimatti. 2006. Formal analysis of hardware requirements. In Proceedings of the 43rd Design Automation Conference (DAC \u201906). E. Sentovich (Ed.), ACM, 821\u2013826."},{"key":"e_1_3_2_76_2","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS \u201977)","author":"Pnueli A.","year":"1977","unstructured":"A. Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS \u201977), 46\u201357."},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_78_2","unstructured":"P. Ralph N. B Ali S. Baltes D. Bianculli J. Diaz Y. Dittrich N. Ernst M. Felderer R. Feldt A. Filieri et al. 2020. Empirical standards for software engineering research. arXiv:2010.03525. Retrieved from https:\/\/github.com\/acmsigsoft\/EmpiricalStandards\/blob\/master\/docs"},{"key":"e_1_3_2_79_2","unstructured":"A. Reid L. Church S. Flur S. de Haas M. Johnson and B. Laurie. 2020. Towards making formal methods normal: Meeting developers where they are. arXiv:2010.16345. Retrieved from https:\/\/arxiv.org\/abs\/2010.16345"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.5555\/41765.41801"},{"key":"e_1_3_2_81_2","first-page":"84","volume-title":"Proceedings of the 5th Workshop on Synthesis (SYNT@CAV \u201916)","volume":"229","author":"Ryzhyk L.","year":"2016","unstructured":"L. Ryzhyk and A. Walker. 2016. Developing a practical reactive synthesis tool: Experience and lessons learned. In Proceedings of the 5th Workshop on Synthesis (SYNT@CAV \u201916). R. Piskac and R. Dimitrova (Eds.), EPTCS, Vol. 229, 84\u201399."},{"key":"e_1_3_2_82_2","first-page":", 666","volume-title":"Proceedings of the 37th IEEE\/ACM International Conference on Software Engineering (ICSE \u201915)","author":"Salman I.","year":"2015","unstructured":"I. Salman, A. T. Misirli, and N. J. Juzgado. 2015. Are students representatives of professionals in software engineering experiments? In Proceedings of the 37th IEEE\/ACM International Conference on Software Engineering (ICSE \u201915). A. Bertolino, G. Canfora, and S. G. Elbaum (Eds.), Vol. 1. IEEE Computer Society, 666\u2013676."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.20"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00030"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91631-2\\_22"},{"issue":"2","key":"e_1_3_2_86_2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/505145.505148","article-title":"Mixin layers: An object-oriented implementation technique for refinements and collaboration-based designs","volume":"11","author":"Smaragdakis Y.","year":"2002","unstructured":"Y. Smaragdakis and D. S. Batory. 2002. Mixin layers: An object-oriented implementation technique for refinements and collaboration-based designs. ACM Transactions on Software Engineering and Methodology 11, 2 (2002), 215\u2013255.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"10","key":"e_1_3_2_87_2","doi-asserted-by":"crossref","first-page":"941","DOI":"10.1109\/32.245736","article-title":"An empirical study of testing and integration strategies using artificial software systems","volume":"19","author":"Solheim J. A.","year":"1993","unstructured":"J. A. Solheim and J. H. Rowland. 1993. An empirical study of testing and integration strategies using artificial software systems. IEEE Transactions on Software Engineering 19, 10 (1993), 941\u2013949.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/3233027.3233029"},{"key":"e_1_3_2_89_2","first-page":"120","volume-title":"Proceedings of the 38th International Conference on Software Engineering (ICSE \u201916)","author":"Stol K.-J.","year":"2016","unstructured":"K.-J. Stol, P. Ralph, and B. Fitzgerald. 2016. Grounded theory in software engineering research: A critical review and guidelines. In Proceedings of the 38th International Conference on Software Engineering (ICSE \u201916). ACM, New York, NY, 120\u2013131."},{"key":"e_1_3_2_90_2","first-page":"117","volume-title":"Proceedings of the 26th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS \u201923)","author":"Sullivan A.","unstructured":"A. Sullivan. 2023. Integrating testing into the alloy model development workflow. In Proceedings of the 26th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS \u201923). IEEE, 117\u2013128."},{"key":"e_1_3_2_91_2","first-page":"1","volume-title":"Proceedings of the 12th Innovations on Software Engineering Conference (Formerly Known as India Software Engineering Conference) (ISEC \u201919)","author":"Tiwari S.","year":"2019","unstructured":"S. Tiwari, D. Ameta, and A. Banerjee. 2019. An approach to identify use case scenarios from textual requirements specification. In Proceedings of the 12th Innovations on Software Engineering Conference (Formerly Known as India Software Engineering Conference) (ISEC \u201919). R. Naik, S. Sarkar, T. T. Hildebrandt, A. Kumar, and R. Sharma (Eds.), ACM, 1\u201311."},{"key":"e_1_3_2_92_2","first-page":"91","volume-title":"Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC\/FSE \u201911)","author":"Treude C.","year":"2011","unstructured":"C. Treude and M.-A. Storey. 2011. Effective communication of software development knowledge through community portals. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC\/FSE \u201911). ACM, New York, NY, 91\u2013101."},{"key":"e_1_3_2_93_2","volume-title":"Exploratory Data Analysis","author":"Tukey J. W.","year":"1977","unstructured":"J. W. Tukey. 1977. Exploratory Data Analysis. Addison-Wesley series in behavioral science: Quantitative methods. Addison-Wesley."},{"key":"e_1_3_2_94_2","first-page":"391","volume-title":"Proceedings of the 31st IEEE International Symposium on Software Reliability Engineering (ISSRE \u201920)","author":"Wang K.","year":"2020","unstructured":"K. Wang, A. Sullivan, D. Marinov, and S. Khurshid. 2020. Fault localization for declarative models in alloy. In Proceedings of the 31st IEEE International Symposium on Software Reliability Engineering (ISSRE \u201920). M. Vieira, H. Madeira, N. Antunes, and Z. Zheng (Eds.), IEEE, 391\u2013402."},{"key":"e_1_3_2_95_2","first-page":"347","volume-title":"Proceedings of the 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering","volume":"1","author":"Waterman M.","year":"2015","unstructured":"M. Waterman, J. Noble, and G. Allan. 2015. How much up-front? A grounded theory of agile architecture. In Proceedings of the 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering, Vol. 1, 347\u2013357."},{"key":"e_1_3_2_96_2","first-page":"313","volume-title":"Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC \u201911)","author":"Wongpiromsarn T.","year":"2011","unstructured":"T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. 2011. TuLiP: A software toolbox for receding horizon temporal logic planning. In Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC \u201911). ACM, New York, NY, 313\u2013314."},{"key":"e_1_3_2_97_2","volume-title":"Case Study Research and Applications","author":"Yin R. K.","year":"2018","unstructured":"R. K. Yin. 2018. Case Study Research and Applications. Sage Thousand Oaks."},{"issue":"3","key":"e_1_3_2_98_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3444689","article-title":"Natural language processing for requirements engineering: A systematic mapping study","volume":"54","author":"Zhao L.","year":"2022","unstructured":"L. Zhao, W. Alhoshan, A. Ferrari, K. J. Letsholo, M. A. Ajagbe, E. Chioasca, and R. T. Batista-Navarro. 2022. Natural language processing for requirements engineering: A systematic mapping study. ACM Computing Surveys 54, 3 (2022), 1\u201341.","journal-title":"ACM Computing Surveys"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3767159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T17:27:19Z","timestamp":1778693239000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3767159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,13]]},"references-count":97,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3767159"],"URL":"https:\/\/doi.org\/10.1145\/3767159","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,5,13]]},"assertion":[{"value":"2024-12-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-26","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}