{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,14]],"date-time":"2026-08-14T18:08:54Z","timestamp":1786730934136,"version":"3.56.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,23]]},"DOI":"10.1145\/3696630.3730562","type":"proceedings-article","created":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:09:27Z","timestamp":1753729767000},"page":"1297-1304","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["RE-oriented Model Development with LLM Support and Deduction-based Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9061-561X","authenticated-orcid":false,"given":"Radoslaw","family":"Klimek","sequence":"first","affiliation":[{"name":"AGH University of Krakow, Krakow, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,7,28]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley."},{"key":"e_1_3_2_1_2_1","volume-title":"Schneider","author":"Alpern Bowen","year":"1985","unstructured":"Bowen Alpern and Fred B. Schneider. 1985. Defining liveness. Inform. Process. Lett. 21 (4) (1985), 181\u2013185."},{"key":"e_1_3_2_1_3_1","unstructured":"ANTLR Development Team. 2023. Website for ANTLR. https:\/\/www.antlr.org\/ accessed on 17-Apr-2023."},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of 10th International Workshop on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD 2005","author":"Araujo Joao","year":"2005","unstructured":"Joao Araujo and Ana Moreira. 2005. Integrating UML Activity Diagrams with Temporal Logic Expressions. In Proceedings of 10th International Workshop on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD 2005), June 13\u201314, 2005, Porto, Portugal. 477\u2013484."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-007-0012-6"},{"key":"e_1_3_2_1_6_1","volume-title":"Merging of Use Case Models: Semantic Foundations. In 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09)","author":"Barrett Stephen","year":"2009","unstructured":"Stephen Barrett, Daniel Sinnig, Patrice Chalin, and Greg Butler. 2009. Merging of Use Case Models: Semantic Foundations. In 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09). 182\u2013189."},{"key":"e_1_3_2_1_7_1","unstructured":"J. Berryman and A. Ziegler. 2024. Prompt Engineering for LLMs: The Art and Science of Building Large Language Model-Based Applications. O'Reilly Media."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-00966-7_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2012.04.005"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"E.M. Clarke J.M. Wing and et al. 1996. Formal methods: State of the art and future directions. Comput. Surveys 28 (4) (1996) 626\u2013643.","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_1_11_1","volume-title":"Handbook of Theoretical Computer Science, Jan van Leeuwen (Ed.).","author":"Emerson Ernest Allen","unstructured":"Ernest Allen Emerson. 1990. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Jan van Leeuwen (Ed.). Vol. B. MIT Press, 995\u20131072. http:\/\/dl.acm.org\/citation.cfm?id=114891.114907"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-FoSE59343.2023.00008"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"e_1_3_2_1_14_1","unstructured":"Marijn Heule Matti J\u00e4rvisalo and Martin Suda. 2022. The international SAT Competitions web page. http:\/\/www.satcompetition.org\/. accessed on 16-May-2022."},{"key":"e_1_3_2_1_15_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"2006","unstructured":"John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley."},{"key":"e_1_3_2_1_16_1","unstructured":"Russell R. Hurlbut. 1997. A Survey of Approaches For Describing and Formalizing Use Cases. Technical Report XPT-TR-97-03. Expertech Ltd."},{"key":"e_1_3_2_1_17_1","volume-title":"24th International Conference on Automated Deduction (CADE 2013","author":"Kaminski Mark","year":"2013","unstructured":"Mark Kaminski and Tobias Tebbi. 2013. In KreSAT: Modal Reasoning via Incremental Reduction to SAT. In 24th International Conference on Automated Deduction (CADE 2013), Lake Placid, New York, 9\u201314 June 2013 (Lecture Notes in Computer Science, Vol. 7898), Maria Paola Bonacina (Ed.). Springer, 436\u2013442."},{"key":"e_1_3_2_1_18_1","unstructured":"Stephen Cole Kleene. 1952. Introduction to Metamathematics. North-Holland."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.02.005"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of Federated Conference on Computer Science and Information Systems (FedCSIS 2013","author":"Klimek Rados\u0142aw","year":"2013","unstructured":"Rados\u0142aw Klimek, \u0141ukasz Faber, and Marek Kisiel-Dorohinicki. 2013. Verifying data integration agents with deduction-based models. In Proceedings of Federated Conference on Computer Science and Information Systems (FedCSIS 2013), 8\u201311 September 2013, Krak\u00f3w, Poland. IEEE Xplore Digital Library, 1049\u20131055."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of Federated Conference on Computer Science and Information Systems (FedCSIS 2013","author":"Klimek Rados\u0142aw","year":"2013","unstructured":"Rados\u0142aw Klimek and Piotr Szwed. 2013. Verification of ArchiMate process specifications based on deductive temporal reasoning. In Proceedings of Federated Conference on Computer Science and Information Systems (FedCSIS 2013), 8\u201311 September 2013, Krak\u00f3w, Poland. IEEE Xplore Digital Library, 1131\u20131138."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 39th IEEE\/ACM International Conference on Automated Software EngineeringWorkshops","author":"Klimek Radoslaw","year":"2024","unstructured":"Radoslaw Klimek and Julia Witek. 2024. Automatic Generation of Logical Specifications for Behavioural Models. In Proceedings of the 39th IEEE\/ACM International Conference on Automated Software EngineeringWorkshops (Sacramento, CA, USA) (ASEW'24). Association for Computing Machinery, New York, NY, USA, 1\u20137. 10.1145\/3695750.3695822"},{"key":"e_1_3_2_1_23_1","volume-title":"The Temporal Logic of Reactive and Concurrent Systems - Specification","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer-Verlag New York, Inc."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1080\/01445340.2015.1084183"},{"key":"e_1_3_2_1_25_1","unstructured":"Tom Pender. 2003. UML Bible. John Wiley & Sons."},{"key":"e_1_3_2_1_26_1","first-page":"3","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov Alexandre","year":"2002","unstructured":"Alexandre Riazanov and Andrei Voronkov. 2002. The design and implementation of VAMPIRE. AI Commun. 15, 2,3 (aug 2002), 91\u2013110.","journal-title":"AI Commun."},{"key":"e_1_3_2_1_27_1","volume-title":"Watson","author":"Runge Tobias","year":"2019","unstructured":"Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Th\u00fcm, Derrick Kourie, and Bruce W. Watson. 2019. Tool Support for Correctness-by-Construction. In Fundamental Approaches to Software Engineering, Reiner H\u00e4hnle and Wil van der Aalst (Eds.). Springer International Publishing, Cham, 25\u201342."},{"key":"e_1_3_2_1_28_1","first-page":"3","article-title":"E - a brainiac theorem prover","volume":"15","author":"Schulz Stephan","year":"2002","unstructured":"Stephan Schulz. 2002. E - a brainiac theorem prover. Journal of AI Communications 15, 2,3 (aug 2002), 111\u2013126.","journal-title":"Journal of AI Communications"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings 2nd Workshop on Formal Methods in the Development of Software, WS-FMDS 2012","volume":"24","author":"Spichkova Maria","year":"2012","unstructured":"Maria Spichkova, Florian H\u00f6lzl, and David Trachtenherz. 2012. Verified System Development with the AutoFocus Tool Chain. In Proceedings 2nd Workshop on Formal Methods in the Development of Software, WS-FMDS 2012, Paris, France, August 28, 2012 (EPTCS, Vol. 86), C\u00e9sar Andr\u00e9s and Luis Llana (Eds.). 17\u201324. 10.4204\/EPTCS.86.3"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-201566"},{"key":"e_1_3_2_1_31_1","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"van Benthem Johan","unstructured":"Johan van Benthem. 1993\u201395. Handbook of Logic in Artificial Intelligence and Logic Programming. Clarendon Press, Chapter Temporal Logic, 241\u2013350."},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of the 36th International Conference on Neural Information Processing Systems","author":"Wei Jason","year":"2022","unstructured":"Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Conference on Neural Information Processing Systems (New Orleans, LA, USA) (NIPS '22). Curran Associates Inc., 24824\u201324837."},{"key":"e_1_3_2_1_33_1","volume-title":"Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL. In 9th International Conference on Business Process Management (BPM 2011","author":"Westergaard Michael","year":"2011","unstructured":"Michael Westergaard. 2011. Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL. In 9th International Conference on Business Process Management (BPM 2011), August 28th - September 2nd 2011, Clermont-Ferrand, France (Lecture Notes in Computer Science, Vol. 6896), Stefanie Rinderle-Ma, Farouk Toumani, and Karsten Wolf (Eds.). Springer, 83\u201398. 10.1007\/978-3-642-23059-2_10"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699697"}],"event":{"name":"FSE Companion '25: 33rd ACM International Conference on the Foundations of Software Engineering","location":"Clarion Hotel Trondheim Trondheim Norway","acronym":"FSE Companion '25","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696630.3730562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:20:27Z","timestamp":1753730427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696630.3730562"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":34,"alternative-id":["10.1145\/3696630.3730562","10.1145\/3696630"],"URL":"https:\/\/doi.org\/10.1145\/3696630.3730562","relation":{},"subject":[],"published":{"date-parts":[[2025,6,23]]},"assertion":[{"value":"2025-07-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}