{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:11Z","timestamp":1781238911625,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":104,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T00:00:00Z","timestamp":1713052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-20-C-0203"],"award-info":[{"award-number":["FA8750-20-C-0203"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,14]]},"DOI":"10.1145\/3644033.3644373","type":"proceedings-article","created":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T16:56:27Z","timestamp":1717692987000},"page":"88-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Methods in Requirements Engineering: Survey and Future Directions"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9242-019X","authenticated-orcid":false,"given":"Robert","family":"Lorch","sequence":"first","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3284-1969","authenticated-orcid":false,"given":"Baoluo","family":"Meng","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5232-1098","authenticated-orcid":false,"given":"Kit","family":"Siu","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7027-2082","authenticated-orcid":false,"given":"Abha","family":"Moitra","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6660-2667","authenticated-orcid":false,"given":"Michael","family":"Durling","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1792-9858","authenticated-orcid":false,"given":"Saswata","family":"Paul","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4620-4266","authenticated-orcid":false,"given":"Sarat Chandra","family":"Varanasi","sequence":"additional","affiliation":[{"name":"GE Aerospace Research, Niskayuna, NY, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8002-791X","authenticated-orcid":false,"given":"Craig","family":"Mcmillan","sequence":"additional","affiliation":[{"name":"GE Aerospace, Evendale, OH, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,6]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"2012 34th International Conference on Software Engineering (ICSE). IEEE, 705--715","author":"Alrajeh Dalal","year":"2012","unstructured":"Dalal Alrajeh, Jeff Kramer, Axel Van Lamsweerde, Alessandra Russo, and Sebastian Uchitel. 2012. Generating obstacle conditions for requirements completeness. In 2012 34th International Conference on Software Engineering (ICSE). IEEE, 705--715."},{"key":"e_1_3_2_1_2_1","volume-title":"2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 676--681","author":"Annervaz KM","year":"2013","unstructured":"KM Annervaz, Vikrant Kaulgud, Shubhashis Sengupta, and Milind Savagaonkar. 2013. Natural language requirements quality analysis based on business domain models. In 2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 676--681."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-006-0029-5"},{"key":"e_1_3_2_1_4_1","volume-title":"A model advisor for NuSMV specifications. Innovations in systems and software engineering 7","author":"Arcaini Paolo","year":"2011","unstructured":"Paolo Arcaini, Angelo Gargantini, and Elvinia Riccobene. 2011. A model advisor for NuSMV specifications. Innovations in systems and software engineering 7 (2011), 97--107."},{"key":"e_1_3_2_1_5_1","volume-title":"2015 International Siberian Conference on Control and Communications (SIBCON). IEEE, 1--4.","author":"Avdeenko Tatiana","year":"2015","unstructured":"Tatiana Avdeenko and Natalia Pustovalova. 2015. The ontology-based approach to support the completeness and consistency of the requirements specification. In 2015 International Siberian Conference on Control and Communications (SIBCON). IEEE, 1--4."},{"key":"e_1_3_2_1_6_1","volume-title":"Vared: Verification and Analysis of Requirements and Early Designs. In 2014 IEEE 22nd International Requirements Engineering Conference (RE). IEEE, 325--326","author":"Badger Julia","year":"2014","unstructured":"Julia Badger, David Throop, and Charles Claunch. 2014. Vared: Verification and Analysis of Requirements and Early Designs. In 2014 IEEE 22nd International Requirements Engineering Conference (RE). IEEE, 325--326."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0330-z"},{"key":"e_1_3_2_1_8_1","volume-title":"Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27--28, 2012. Proceedings 17","author":"Barnat Jiri","year":"2012","unstructured":"Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, and Petr Ro\u0107kai. 2012. Tool chain to support automated formal verification of avionics simulink designs. In Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27--28, 2012. Proceedings 17. Springer, 78--92."},{"key":"e_1_3_2_1_9_1","unstructured":"Saddek Bensalem Vijay Ganesh Yassine Lakhnech C\u00e9sar Munoz Sam Owre Harald Rue\u00df John Rushby Vlad Rusu Hassen Saiedi and Natarajan Shankar. 2000. An overview of SAL. In Lfm2000: Fifth NASA Langley Formal Methods Workshop."},{"key":"e_1_3_2_1_10_1","volume-title":"4th Workshop on Formal Integrated Development Environment.","author":"Bhatt Devesh","year":"2018","unstructured":"Devesh Bhatt, Anitha Murugesan, Brendan Hall, Hao Ren, and Yogananda Jeppu. 2018. The CLEAR way to transparent formal methods. In 4th Workshop on Formal Integrated Development Environment."},{"key":"e_1_3_2_1_11_1","volume-title":"Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems at 18th International Conference on Formal Engineering Methods.","author":"Bienm\u00fcller Tom","year":"2016","unstructured":"Tom Bienm\u00fcller, Tino Teige, Andreas Eggers, and Matthias Stasch. 2016. Modeling requirements for quantitative consistency analysis and automatic test case generation. In Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems at 18th International Conference on Formal Engineering Methods."},{"key":"e_1_3_2_1_12_1","volume-title":"Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15--19, 2010. Proceedings 22","author":"Bloem Roderick","year":"2010","unstructured":"Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert K\u00f6nighofer, Marco Roveri, Viktor Schuppan, and Richard Seeber. 2010. RATSY-a new requirements analysis tool with synthesis. In Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15--19, 2010. Proceedings 22. Springer, 425--429."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010193"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0387-x"},{"key":"e_1_3_2_1_15_1","volume-title":"2009 IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 665--667","author":"Cavada Roberto","year":"2009","unstructured":"Roberto Cavada, Alessandro Cimatti, Alessandro Mariotti, Cristian Mattarei, Andrea Micheli, Sergio Mover, Marco Pensallorto, Marco Roveri, Angelo Susi, and Stefano Tonetta. 2009. Supporting requirements validation: The EuRailCheck tool. In 2009 IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 665--667."},{"key":"e_1_3_2_1_16_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS","author":"Chamarthi Harsh Raju","year":"2011","unstructured":"Harsh Raju Chamarthi, Peter Dillinger, Panagiotis Manolios, and Daron Vroon. 2011. The ACL2 Sedan theorem proving system. In Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26--April 3, 2011. Proceedings 17. Springer, 291--295."},{"key":"e_1_3_2_1_17_1","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II. Springer, 510--517","author":"Champion Adrien","year":"2016","unstructured":"Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 model checker. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II. Springer, 510--517."},{"key":"e_1_3_2_1_18_1","volume-title":"2019 IEEE 27th International Requirements Engineering Conference (RE). IEEE, 308--318","author":"Chen Xiaohong","year":"2019","unstructured":"Xiaohong Chen, Zhiwei Zhong, Zhi Jin, Min Zhang, Tong Li, Xiang Chen, and Tingliang Zhou. 2019. Automating consistency verification of safety requirements for railway interlocking systems. In 2019 IEEE 27th International Requirements Engineering Conference (RE). IEEE, 308--318."},{"key":"e_1_3_2_1_19_1","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part I. Springer, 95--117","author":"Cheng Chih-Hong","year":"2016","unstructured":"Chih-Hong Cheng, Yassine Hamza, and Harald Ruess. 2016. Structural synthesis for GXW specifications. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part I. Springer, 95--117."},{"key":"e_1_3_2_1_20_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS","author":"Cheng Chih-Hong","year":"2017","unstructured":"Chih-Hong Cheng, Edward A Lee, and Harald Ruess. 2017. autoCode4: structural controller synthesis. In Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings, Part I 23. Springer, 398--404."},{"key":"e_1_3_2_1_21_1","volume-title":"Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27--31, 2002 Proceedings 14","author":"Cimatti Alessandro","year":"2002","unstructured":"Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2002. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27--31, 2002 Proceedings 14. Springer, 359--364."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1142\/S1793351X13500025"},{"key":"e_1_3_2_1_23_1","volume-title":"2017 IEEE 25th International Requirements Engineering Conference (RE). IEEE, 283--291","author":"Crapo Andrew","year":"2017","unstructured":"Andrew Crapo, Abha Moitra, Craig McMillan, and Daniel Russell. 2017. Requirements capture and analysis in ASSERT (TM). In 2017 IEEE 25th International Requirements Engineering Conference (RE). IEEE, 283--291."},{"key":"e_1_3_2_1_24_1","volume-title":"2019 IEEE 13th International Conference on Semantic Computing (ICSC). IEEE, 361--366","author":"Crapo Andrew W","year":"2019","unstructured":"Andrew W Crapo and Abha Moitra. 2019. Using OWL ontologies as a domain-specific language for capturing requirements for formal analysis and test case generation. In 2019 IEEE 13th International Conference on Semantic Computing (ICSC). IEEE, 361--366."},{"key":"e_1_3_2_1_25_1","first-page":"449","article-title":"Generating typed dependency parses from phrase structure parses","volume":"6","author":"De Marneffe Marie-Catherine","year":"2006","unstructured":"Marie-Catherine De Marneffe, Bill MacCartney, Christopher D Manning, et al. 2006. Generating typed dependency parses from phrase structure parses.. In Lrec, Vol. 6. 449--454.","journal-title":"Lrec"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 40th International Conference on Software Engineering. 1125--1135","author":"Degiovanni Renzo","year":"2018","unstructured":"Renzo Degiovanni, Pablo Castro, Marcelo Arroyo, Marcelo Ruiz, Nazareno Aguirre, and Marcelo Frias. 2018. Goal-conflict likelihood assessment based on model counting. In Proceedings of the 40th International Conference on Software Engineering. 1125--1135."},{"key":"e_1_3_2_1_27_1","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II 28","author":"Ehlers R\u00fcdiger","year":"2016","unstructured":"R\u00fcdiger Ehlers and Vasumathi Raman. 2016. Slugs: Extensible gr (1) synthesis. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II 28. Springer, 333--339."},{"key":"e_1_3_2_1_28_1","volume-title":"2006 IEEE conference on computer aided control system design, 2006 IEEE international conference on control applications, 2006 IEEE international symposium on intelligent control. IEEE, 1206--1211","author":"Feiler Peter H","year":"2006","unstructured":"Peter H Feiler, Bruce A Lewis, and Steve Vestal. 2006. The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems. In 2006 IEEE conference on computer aided control system design, 2006 IEEE international conference on control applications, 2006 IEEE international symposium on intelligent control. IEEE, 1206--1211."},{"key":"e_1_3_2_1_29_1","volume-title":"NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings 9. Springer, 420--426","author":"Fifarek Aaron W","year":"2017","unstructured":"Aaron W Fifarek, Lucas G Wagner, Jonathan A Hoffman, Benjamin D Rodes, M Anthony Aiello, and Jennifer A Davis. 2017. SpeAR v2. 0: Formalized past LTL specification and analysis of requirements. In NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings 9. Springer, 420--426."},{"key":"e_1_3_2_1_30_1","volume-title":"Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part II 30","author":"Gacek Andrew","year":"2018","unstructured":"Andrew Gacek, John Backes, Mike Whalen, Lucas Wagner, and Elaheh Ghassabani. 2018. The JKind model checker. In Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part II 30. Springer, 20--27."},{"key":"e_1_3_2_1_31_1","volume-title":"NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27--29, 2015, Proceedings 7. Springer, 173--187","author":"Gacek Andrew","year":"2015","unstructured":"Andrew Gacek, Andreas Katis, Michael W Whalen, John Backes, and Darren Cofer. 2015. Towards realizability checking of contracts using theories. In NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27--29, 2015, Proceedings 7. Springer, 173--187."},{"key":"e_1_3_2_1_32_1","unstructured":"Daniel Galin. 2004. Software quality assurance: from theory to implementation. Pearson education."},{"key":"e_1_3_2_1_33_1","volume-title":"Ontological approach to checking event consistency for a set of temporal requirements. In 2019 International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON)","author":"Garanina Natalia","unstructured":"Natalia Garanina and Olesya Borovikova. 2019. Ontological approach to checking event consistency for a set of temporal requirements. In 2019 International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON). IEEE, 0922--0927."},{"key":"e_1_3_2_1_34_1","volume-title":"Integrated Formal Methods: 9th International Conference, IFM 2012, Pisa, Italy, June 18--21, 2012. Proceedings 9. Springer, 312--326","author":"Garis Ana","year":"2012","unstructured":"Ana Garis, Ana CR Paiva, Alcino Cunha, and Daniel Riesco. 2012. Specifying UML protocol state machines in alloy. In Integrated Formal Methods: 9th International Conference, IFM 2012, Pisa, Italy, June 18--21, 2012. Proceedings 9. Springer, 312--326."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1072997.1072999"},{"key":"e_1_3_2_1_36_1","volume-title":"Automatically extracting requirements specifications from natural language. arXiv preprint arXiv:1403.3142","author":"Ghosh Shalini","year":"2014","unstructured":"Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. 2014. Automatically extracting requirements specifications from natural language. arXiv preprint arXiv:1403.3142 (2014)."},{"key":"e_1_3_2_1_37_1","volume-title":"NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7--9, 2016, Proceedings 8. Springer, 41--46","author":"Ghosh Shalini","year":"2016","unstructured":"Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. 2016. ARSENAL: automatic requirements specification extraction from natural language. In NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7--9, 2016, Proceedings 8. Springer, 41--46."},{"key":"e_1_3_2_1_38_1","volume-title":"International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020)","author":"Giannakopoulou Dimitra","year":"2020","unstructured":"Dimitra Giannakopoulou, Anastasia Mavridou, Julian Rhein, Thomas Pressburger, Johann Schumann, and Nija Shi. 2020. Formal requirements elicitation with FRET. In International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"e_1_3_2_1_41_1","volume-title":"Trust Management: Third International Conference, iTrust 2005, Paris, France, May 23--26, 2005. Proceedings 3. Springer, 415--419","author":"Giorgini Paolo","year":"2005","unstructured":"Paolo Giorgini, Fabio Massacci, John Mylopoulos, Alberto Siena, and Nicola Zannone. 2005. ST-Tool: A CASE tool for modeling and analyzing trust requirements. In Trust Management: Third International Conference, iTrust 2005, Paris, France, May 23--26, 2005. Proceedings 3. Springer, 415--419."},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. 433--443","author":"Greenyer Joel","year":"2013","unstructured":"Joel Greenyer, Christian Brenner, Maxime Cordy, Patrick Heymans, and Erika Gressi. 2013. Incrementally synthesizing controllers from scenario-based product line specifications. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. 433--443."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-013-0169-4"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2016.16"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_46_1","volume-title":"Jan Fiedor, Joaqu\u00edn Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, and Gopal Gupta.","author":"Hall Brendan","year":"2021","unstructured":"Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaqu\u00edn Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, and Gopal Gupta. 2021. Knowledge-assisted reasoning of model-augmented system requirements with event calculus and goal-directed answer set programming. arXiv preprint arXiv:2109.04634 (2021)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCIS.2013.511"},{"key":"e_1_3_2_1_48_1","volume-title":"2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1166--1169","author":"Huang Yihao","year":"2019","unstructured":"Yihao Huang, Jincao Feng, Hanyue Zheng, Jiayi Zhu, Shang Wang, Siyuan Jiang, Weikai Miao, and Geguang Pu. 2019. Prema: a tool for precise requirements editing, modeling and analysis. In 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1166--1169."},{"key":"e_1_3_2_1_49_1","volume-title":"Logic in Computer Science: Modelling and reasoning about systems","author":"Huth Michael","unstructured":"Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/129393.129398"},{"key":"e_1_3_2_1_51_1","volume-title":"2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES). IEEE, 140--149","author":"Jahier Erwan","year":"2013","unstructured":"Erwan Jahier, Nicolas Halbwachs, and Pascal Raymond. 2013. Engineering functional requirements of reactive systems using synchronous languages. In 2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES). IEEE, 140--149."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(97)00171-4"},{"key":"e_1_3_2_1_53_1","volume-title":"Capture","author":"Katis Andreas","year":"2022","unstructured":"Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger, and Johann Schumann. 2022. Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET. In Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7--10, 2022, Proceedings, Part II. Springer, 490--504."},{"key":"e_1_3_2_1_54_1","volume-title":"International journal on software tools for technology transfer 15, 5--6","author":"K\u00f6nighofer Robert","year":"2013","unstructured":"Robert K\u00f6nighofer, Georg Hofferek, and Roderick Bloem. 2013. Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. International journal on software tools for technology transfer 15, 5--6 (2013), 563--583."},{"key":"e_1_3_2_1_55_1","volume-title":"2019 IEEE 27th International Requirements Engineering Conference (RE). IEEE, 234--244","author":"Langenfeld Vincent","year":"2019","unstructured":"Vincent Langenfeld, Daniel Dietsch, Bernd Westphal, Jochen Hoenicke, and Amalinda Post. 2019. Scalable analysis of real-time requirements. In 2019 IEEE 27th International Requirements Engineering Conference (RE). IEEE, 234--244."},{"key":"e_1_3_2_1_56_1","volume-title":"2008 16th IEEE International Requirements Engineering Conference. IEEE, 193--202","author":"Lauenroth Kim","year":"2008","unstructured":"Kim Lauenroth and Klaus Pohl. 2008. Dynamic consistency checking of domain requirements in product line engineering. In 2008 16th IEEE International Requirements Engineering Conference. IEEE, 193--202."},{"key":"e_1_3_2_1_58_1","volume-title":"2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC). IEEE, 1--10","author":"Li Meng","year":"2019","unstructured":"Meng Li, Baoluo Meng, Han Yu, Kit Siu, Michael Durling, Daniel Russell, Craig McMillan, Matthew Smith, Mark Stephens, and Scott Thomson. 2019. Requirements-based automated test generation for safety critical software. In 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC). IEEE, 1--10."},{"key":"e_1_3_2_1_59_1","volume-title":"Requirements Engineering: Foundation for Software Quality: 20th International Working Conference, REFSQ 2014, Essen, Germany, April 7--10, 2014. Proceedings 20","author":"Li Wenbin","year":"2014","unstructured":"Wenbin Li, David Brown, Jane Huffman Hayes, and Miroslaw Truszczynski. 2014. Answer-set programming in requirements engineering. In Requirements Engineering: Foundation for Software Quality: 20th International Working Conference, REFSQ 2014, Essen, Germany, April 7--10, 2014. Proceedings 20. Springer, 168--183."},{"key":"e_1_3_2_1_60_1","volume-title":"Workshop on Language and Robotics at CoRL","author":"Liu Jason Xinyu","year":"2022","unstructured":"Jason Xinyu Liu, Ziyi Yang, Benjamin Schornstein, Sam Liang, Ifrah Idrees, Stefanie Tellex, and Ankit Shah. 2022. Lang2ltl: Translating natural language commands to temporal specification with large language models. In Workshop on Language and Robotics at CoRL 2022."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897667.2897668"},{"key":"e_1_3_2_1_62_1","volume-title":"NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings 9. Springer, 427--434","author":"L\u00facio Levi","year":"2017","unstructured":"Levi L\u00facio, Salman Rahman, Chih-Hong Cheng, and Alistair Mavin. 2017. Just formal enough? automated analysis of EARS requirements. In NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings 9. Springer, 427--434."},{"key":"e_1_3_2_1_63_1","volume-title":"2016 Federated Conference on Computer Science and Information Systems (FedCSIS). IEEE, 1737--1746","author":"Mahmud Nesredin","year":"2016","unstructured":"Nesredin Mahmud, Cristina Seceleanu, and Oscar Ljungkrantz. 2016. Resa tool: Structured requirements specification and sat-based consistency-checking. In 2016 Federated Conference on Computer Science and Information Systems (FedCSIS). IEEE, 1737--1746."},{"key":"e_1_3_2_1_64_1","first-page":"639","article-title":"Scalable methods for analyzing formalized requirements and localizing errors","volume":"9","author":"Manolios Panagiotis","year":"2017","unstructured":"Panagiotis Manolios. 2017. Scalable methods for analyzing formalized requirements and localizing errors. US Patent 9,639,450.","journal-title":"US Patent"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-021-00868-z"},{"key":"e_1_3_2_1_66_1","volume-title":"Proceedings of the tenth international conference on Aspect-oriented software development. 19--30","author":"Maoz Shahar","year":"2011","unstructured":"Shahar Maoz and Yaniv Sa'ar. 2011. AspectLTL: an aspect language for LTL specifications. In Proceedings of the tenth international conference on Aspect-oriented software development. 19--30."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","article-title":"Proving the shalls: Early validation of requirements through formal methods","volume":"8","author":"Miller Steven P","year":"2006","unstructured":"Steven P Miller, Alan C Tribble, Michael W Whalen, and Mats PE Heimdahl. 2006. Proving the shalls: Early validation of requirements through formal methods. International Journal on Software Tools for Technology Transfer 8 (2006), 303--319.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"crossref","first-page":"e6702","DOI":"10.1002\/cpe.6702","article-title":"A review on security requirements specification by formal methods","volume":"34","author":"Mishra Aditya Dev","year":"2022","unstructured":"Aditya Dev Mishra and Khurram Mustafa. 2022. A review on security requirements specification by formal methods. Concurrency and Computation: Practice and Experience 34, 5 (2022), e6702.","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-019-00316-x"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3197281"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-010-9135-4"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-019-00339-1"},{"key":"e_1_3_2_1_74_1","volume-title":"International Working Conference on Requirements Engineering: Foundation for Software Quality. Springer, 87--95","author":"Nayak Anmol","year":"2022","unstructured":"Anmol Nayak, Hari Prasad Timmapathini, Vidhya Murali, Karthikeyan Ponnalagu, Vijendran Gopalan Venkoparao, and Amalinda Post. 2022. Req2Spec: Transforming software requirements into formal specifications using natural language processing. In International Working Conference on Requirements Engineering: Foundation for Software Quality. Springer, 87--95."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-013-9202-6"},{"key":"e_1_3_2_1_76_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 839--844","author":"Nuzzo Pierluigi","year":"2018","unstructured":"Pierluigi Nuzzo, Michele Lora, Yishai A Feldman, and Alberto L Sangiovanni-Vincentelli. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 839--844."},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-2648-4"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.5120\/12020-8017","article-title":"Formal Methods in Requirements Phase of SDLC","volume":"70","author":"Pandey SK","year":"2013","unstructured":"SK Pandey and Mona Batra. 2013. Formal Methods in Requirements Phase of SDLC. International Journal of Computer Applications 70, 13 (2013), 7--14.","journal-title":"International Journal of Computer Applications"},{"key":"e_1_3_2_1_80_1","volume-title":"Engineering and Management: 12th International Conference, KSEM 2019, Athens, Greece, August 28--30, 2019, Proceedings, Part II 12","author":"Pi Xingxing","year":"2019","unstructured":"Xingxing Pi, Jianqi Shi, Yanhong Huang, and Hansheng Wei. 2019. Automated Mining and Checking of Formal Properties in Natural Language Requirements. In Knowledge Science, Engineering and Management: 12th International Conference, KSEM 2019, Athens, Greece, August 28--30, 2019, Proceedings, Part II 12. Springer, 75--87."},{"key":"e_1_3_2_1_81_1","volume-title":"VMCAI 2006, Charleston, SC, USA, January 8--10, 2006. Proceedings 7. Springer, 364--380","author":"Piterman Nir","year":"2006","unstructured":"Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. 2006. Synthesis of reactive (1) designs. In Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8--10, 2006. Proceedings 7. Springer, 364--380."},{"key":"e_1_3_2_1_82_1","volume-title":"The economic impacts of inadequate infrastructure for software testing","author":"Planning Strategic","year":"2002","unstructured":"Strategic Planning. 2002. The economic impacts of inadequate infrastructure for software testing. National Institute of Standards and Technology 1 (2002)."},{"key":"e_1_3_2_1_83_1","volume-title":"A platform for requirement based formal specification. In 2008 Forum on Specification, Verification and Design Languages","author":"Pro\u00df Uwe","unstructured":"Uwe Pro\u00df, Erik Markert, Jan Langer, Andreas Richter, Chris Drechsler, and Ulrich Heinkel. 2008. A platform for requirement based formal specification. In 2008 Forum on Specification, Verification and Design Languages. IEEE, 237--238."},{"key":"e_1_3_2_1_84_1","volume-title":"2017 IEEE 25th International Requirements Engineering Conference Workshops (REW). IEEE, 331--338","author":"Robinson-Mallett Christopher L","year":"2017","unstructured":"Christopher L Robinson-Mallett and Robert M Hierons. 2017. Integrating graphical and natural language specifications to support analysis and testing. In 2017 IEEE 25th International Requirements Engineering Conference Workshops (REW). IEEE, 331--338."},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2011.2166784"},{"key":"e_1_3_2_1_87_1","volume-title":"Proceedings of the 27th Annual ACM Symposium on Applied Computing. 1063--1068","author":"Scandurra Patrizia","year":"2012","unstructured":"Patrizia Scandurra, Andrea Arnoldi, Tao Yue, and Marco Dolci. 2012. Functional requirements validation by transforming use case models into Abstract State Machines. In Proceedings of the 27th Annual ACM Symposium on Applied Computing. 1063--1068."},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.33"},{"key":"e_1_3_2_1_89_1","volume-title":"Artificial intelligence today: Recent trends and developments","author":"Shanahan Murray","unstructured":"Murray Shanahan. 2001. The Event Calculus Explained. In Artificial intelligence today: Recent trends and developments. Springer, 409--430."},{"key":"e_1_3_2_1_90_1","volume-title":"Requirements Engineering: Foundation for Software Quality: 16th International Working Conference, REFSQ 2010, Essen, Germany, June 30--July 2, 2010. Proceedings 16","author":"Sikora Ernst","year":"2010","unstructured":"Ernst Sikora, Marian Daun, and Klaus Pohl. 2010. Supporting the consistent specification of scenarios across multiple abstraction levels. In Requirements Engineering: Foundation for Software Quality: 16th International Working Conference, REFSQ 2010, Essen, Germany, June 30--July 2, 2010. Proceedings 16. Springer, 45--59."},{"key":"e_1_3_2_1_91_1","volume-title":"2017 IEEE\/AIAA 36th Digital Avionics Systems Conference (DASC). IEEE, 1--10","author":"Siu Kit","year":"2017","unstructured":"Kit Siu, Abha Moitra, Michael Durling, Andy Crapo, Meng Li, Han Yu, Heber Herencia-Zapana, Mauricio Castillo-Effen, Shiraj Sen, Craig McMillan, et al. 2017. Flight critical software and systems development using ASSERT. In 2017 IEEE\/AIAA 36th Digital Avionics Systems Conference (DASC). IEEE, 1--10."},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/2898375.2898381"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.5"},{"key":"e_1_3_2_1_94_1","volume-title":"2013 21st IEEE International Requirements Engineering Conference (RE). IEEE, 330--331","author":"Teufl Sabine","year":"2013","unstructured":"Sabine Teufl, Dongyue Mou, and Daniel Ratiu. 2013. MIRA: A Tooling-Framework to Experiment with Model-Based Requirements Engineering. In 2013 21st IEEE International Requirements Engineering Conference (RE). IEEE, 330--331."},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-011-0204-1"},{"key":"e_1_3_2_1_96_1","volume-title":"2013 20th Asia-Pacific Software Engineering Conference (APSEC)","volume":"1","author":"Traichaiyaporn Kriangkrai","year":"2013","unstructured":"Kriangkrai Traichaiyaporn and Toshiaki Aoki. 2013. Preserving correctness of requirements evolution through refinement in event-b. In 2013 20th Asia-Pacific Software Engineering Conference (APSEC), Vol. 1. IEEE, 315--322."},{"key":"e_1_3_2_1_97_1","volume-title":"2011 IEEE 19th International Requirements Engineering Conference. IEEE, 143--152","author":"Ubayashi Naoyasu","year":"2011","unstructured":"Naoyasu Ubayashi, Yasutaka Kamei, Masayuki Hirayama, and Tetsuo Tamai. 2011. A context analysis method for embedded systems---Exploring a requirement boundary between a system and its context. In 2011 IEEE 19th International Requirements Engineering Conference. IEEE, 143--152."},{"key":"e_1_3_2_1_98_1","volume-title":"International Symposium on Practical Aspects of Declarative Languages. Springer, 181--190","author":"Varanasi Sarat Chandra","year":"2022","unstructured":"Sarat Chandra Varanasi, Joaquin Arias, Elmer Salazar, Fang Li, Kinjal Basu, and Gopal Gupta. 2022. Modeling and Verification of Real-Time Systems with the Event Calculus and s (CASP). In International Symposium on Practical Aspects of Declarative Languages. Springer, 181--190."},{"key":"e_1_3_2_1_99_1","volume-title":"2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST). IEEE, 363--366","author":"Vuotto Simone","year":"2019","unstructured":"Simone Vuotto, Massimo Narizzano, Luca Pulina, and Armando Tacchella. 2019. Poster: Automatic consistency checking of requirements with ReqV. In 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST). IEEE, 363--366."},{"key":"e_1_3_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-009-0123-6"},{"key":"e_1_3_2_1_101_1","volume-title":"2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). IEEE, 78--84","author":"Wakrime Abderrahim Ait","year":"2018","unstructured":"Abderrahim Ait Wakrime, J Paul Gibson, and Jean-Luc Raffy. 2018. Formalising the requirements of an E-voting software product line using Event-B. In 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). IEEE, 78--84."},{"key":"e_1_3_2_1_102_1","volume-title":"2017 IEEE 25th International Requirements Engineering Conference (RE). IEEE, 263--272","author":"Walter Benedikt","year":"2017","unstructured":"Benedikt Walter, Jakob Hammes, Marco Piechotta, and Stephan Rudolph. 2017. A formalization method to process structured natural language to logic expressions to detect redundant specification and test statements. In 2017 IEEE 25th International Requirements Engineering Conference (RE). IEEE, 263--272."},{"key":"e_1_3_2_1_103_1","volume-title":"2020 6th International Symposium on System and Software Reliability (ISSSR). IEEE, 12--20","author":"Wang WenXuan","year":"2020","unstructured":"WenXuan Wang, Jun Hu, JianChen Hu, JieXiang Kang, Hui Wang, and ZhongJie Gao. 2020. Automatic test case generation from formal requirement model for avionics software. In 2020 6th International Symposium on System and Software Reliability (ISSSR). IEEE, 12--20."},{"key":"e_1_3_2_1_104_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1677--1682","author":"Yan Rongjie","year":"2015","unstructured":"Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. 2015. Formal consistency checking over specifications in natural languages. In 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1677--1682."},{"key":"e_1_3_2_1_105_1","volume-title":"Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation. arXiv preprint arXiv:2305.15541","author":"Yang Yuan","year":"2023","unstructured":"Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2023. Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation. arXiv preprint arXiv:2305.15541 (2023)."},{"key":"e_1_3_2_1_106_1","volume-title":"MBIPV: a model-based approach for identifying privacy violations from software requirements. Software and Systems Modeling","author":"Ye Tong","year":"2022","unstructured":"Tong Ye, Yi Zhuang, and Gongzhe Qiao. 2022. MBIPV: a model-based approach for identifying privacy violations from software requirements. Software and Systems Modeling (2022), 1--30."},{"key":"e_1_3_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10845-021-01753-8"},{"key":"e_1_3_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2010.12.010"}],"event":{"name":"FormaliSE '24: 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)","location":"Lisbon Portugal","acronym":"FormaliSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644373","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3644033.3644373","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:58Z","timestamp":1750291018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644373"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,14]]},"references-count":104,"alternative-id":["10.1145\/3644033.3644373","10.1145\/3644033"],"URL":"https:\/\/doi.org\/10.1145\/3644033.3644373","relation":{},"subject":[],"published":{"date-parts":[[2024,4,14]]},"assertion":[{"value":"2024-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}