{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T05:08:59Z","timestamp":1770354539623,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031917592","type":"print"},{"value":"9783031917608","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-91760-8_10","type":"book-chapter","created":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T16:57:48Z","timestamp":1748537868000},"page":"138-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the\u00a0Role of\u00a0Generative AI in\u00a0Explaining Model Checking Counterexamples"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9511-6932","authenticated-orcid":false,"given":"Ezequiel Jos\u00e9 Veloso Ferreira","family":"Moreira","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-580X","authenticated-orcid":false,"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,30]]},"reference":[{"key":"10_CR1","unstructured":"Bachert, M., Hesenius, M.: Synthesizing 2d vs. 3d gestures. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"issue":"2","key":"10_CR2","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/1061254.1061256","volume":"14","author":"J Berstel","year":"2005","unstructured":"Berstel, J., Reghizzi, S.C., Roussel, G., Pietro, P.S.: A scalable formal method for design and automatic checking of user interfaces. ACM Trans. Softw. Eng. Methodol. 14(2), 124\u2013167 (2005). https:\/\/doi.org\/10.1145\/1061254.1061256","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10_CR3","unstructured":"Bisante, A., Datla, V.S.V., Panizzi, E., Trasciatti, G., Zeppieri, S.: Assessing large language models adoption in need finding: an exploratory study. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bisante, A., Datla, V.S.V., Panizzi, E., Trasciatti, G., Zeppieri, S.: Enhancing interface design with AI: an exploratory study on a ChatGPT-4-based tool for cognitive walkthrough inspired evaluations. In: Proceedings of the 2024 International Conference on Advanced Visual Interfaces. ACM (2024). https:\/\/doi.org\/10.1145\/3656650.3656676","DOI":"10.1145\/3656650.3656676"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Bisante, A., Dix, A., Panizzi, E., Zeppieri, S.: To err is AI. In: Proceedings of the 15th Biannual Conference of the Italian SIGCHI Chapter. ACM, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3605390.3605414","DOI":"10.1145\/3605390.3605414"},{"issue":"3","key":"10_CR6","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1109\/TSMCA.2012.2210406","volume":"43","author":"ML Bolton","year":"2013","unstructured":"Bolton, M.L., Bass, E., Siminiceanu, R.: Using formal verification to evaluate human-automation interaction: a review. IEEE Trans. Syst. Man Cybern. Part A Syst. Hum. 43(3), 488\u2013503 (2013). https:\/\/doi.org\/10.1109\/TSMCA.2012.2210406","journal-title":"IEEE Trans. Syst. Man Cybern. Part A Syst. Hum."},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Campos, J., Harrison, M.D.: Interaction engineering using the IVY tool. In: ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pp. 35\u201344. ACM (2009). https:\/\/doi.org\/10.1145\/1570433.1570442","DOI":"10.1145\/1570433.1570442"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"315","DOI":"10.5772\/56412","volume":"10","author":"J Campos","year":"2013","unstructured":"Campos, J., Machado, J.: A specification patterns system for discrete event systems\u2019 analysis. Int. J. Adv. Rob. Syst. 10, 315 (2013). https:\/\/doi.org\/10.5772\/56412","journal-title":"Int. J. Adv. Rob. Syst."},{"issue":"3\/4","key":"10_CR9","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1023\/A:1011265604021","volume":"8","author":"JC Campos","year":"2001","unstructured":"Campos, J.C., Harrison, M.D.: Model checking interactor specifications. Autom. Softw. Eng. 8(3\/4), 275\u2013310 (2001). https:\/\/doi.org\/10.1023\/A:1011265604021","journal-title":"Autom. Softw. Eng."},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"10_CR11","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"10_CR12","unstructured":"Coppens, A., Maquil, V.: Integrating AIs with body tracking technology for human behaviour analysis: challenges and opportunities. In: Engineering Interactive Systems Embedding AI Technologies workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR13","unstructured":"Dittmar, A., Forbrig, P.: Revisiting usability in the current era of AI. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Duan, P., Warner, J., Hartmann, B.: Towards generating UI design feedback with LLMs. In: Adjunct Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology. ACM, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3586182.3615810","DOI":"10.1145\/3586182.3615810"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of 21st International Conference on Software Engineering, pp. 411\u2013420. ACM (1999). https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Feldt, R., de\u00a0Oliveira\u00a0Neto, F.G., Torkar, R.: Ways of applying artificial intelligence in software engineering. In: 2018 IEEE\/ACM 6th International Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE 2018), pp. 35\u201341 (2018). https:\/\/doi.org\/10.1145\/3194104.3194109","DOI":"10.1145\/3194104.3194109"},{"key":"10_CR17","unstructured":"Gross, G.: Devs gaining little (if anything) from AI coding assistants. CIO, September 26 2024. https:\/\/www.cio.com\/article\/3540579\/devs-gaining-little-if-anything-from-ai-coding-assistants.html"},{"key":"10_CR18","unstructured":"Harrison, M., Thimbleby, H. (eds.): Formal Methods in Human-Computer Interaction. Cambridge University Press, Cambridge Series on Human-Computer Interaction (1990)"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1111\/beer.12479","volume":"32","author":"L Illia","year":"2023","unstructured":"Illia, L., Colleoni, E., Zyglidopoulos, S.: Ethical implications of text generation in the age of artificial intelligence. Bus. Ethics Environ. Responsib. 32(1), 201\u2013210 (2023). https:\/\/doi.org\/10.1111\/beer.12479","journal-title":"Bus. Ethics Environ. Responsib."},{"key":"10_CR20","unstructured":"Luyten, K., Eerlings, G., Liesenborgs, J., Ruiz, G.R., Vanbrabant, S., Vanacken, D.: Opportunities and challenges of model multiplicity in interactive software systems. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR21","unstructured":"Menten, R., Ruiz, G.R., Vanacken, D.: NexOz - a Wizard of Oz approach to facilitate the integration of AI in interactive systems. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR22","unstructured":"Mereu, J., et al.: Empowering end-user in creating extended reality content with a conversational chatbot. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Moreira, E., Campos, J.: A language for explaining counterexamples. In: 13th Symposium on Languages, Applications and Technologies (SLATE 2024). OpenAccess Series in Informatics (OASIcs), vol.\u00a0120, pp. 11:1\u201311:14. Schloss Dagstuhl - LZI (2024). https:\/\/doi.org\/10.4230\/OASIcs.SLATE.2024.11","DOI":"10.4230\/OASIcs.SLATE.2024.11"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds.): The Handbook of Formal Methods in Human-Computer Interaction. HIS, Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-51838-1","DOI":"10.1007\/978-3-319-51838-1"},{"issue":"7","key":"10_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3626314","volume":"56","author":"J Perez-Cerrolaza","year":"2024","unstructured":"Perez-Cerrolaza, J., et al.: Artificial intelligence for safety-critical systems in industrial and transportation domains: a survey. ACM Comput. Surv. 56(7), 1\u201340 (2024). https:\/\/doi.org\/10.1145\/3626314","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"10_CR26","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J Rushby","year":"2002","unstructured":"Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliab. Eng. Syst. Saf. 75(2), 167\u2013177 (2002). https:\/\/doi.org\/10.1016\/S0951-8320(01)00092-8","journal-title":"Reliab. Eng. Syst. Saf."},{"issue":"1","key":"10_CR27","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/3637436","volume":"31","author":"A Schmidt","year":"2024","unstructured":"Schmidt, A., Elagroudy, P., Draxler, F., Kreuter, F., Welsch, R.: Simulating the human in HCD with ChatGPT: redesigning interaction design with AI. Interactions 31(1), 24\u201331 (2024). https:\/\/doi.org\/10.1145\/3637436","journal-title":"Interactions"},{"issue":"9","key":"10_CR28","doi-asserted-by":"publisher","DOI":"10.1098\/rsos.231053","volume":"10","author":"W Tabone","year":"2023","unstructured":"Tabone, W., de Winter, J.: Using ChatGPT for human-computer interaction research: a primer. R. Soc. Open Sci. 10(9), 231053 (2023). https:\/\/doi.org\/10.1098\/rsos.231053","journal-title":"R. Soc. Open Sci."},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-76805-0_1","volume-title":"HCI and Usability for Medicine and Health Care","author":"H Thimbleby","year":"2007","unstructured":"Thimbleby, H.: User-centered methods are insufficient for safety critical systems. In: Holzinger, A. (ed.) USAB 2007. LNCS, vol. 4799, pp. 1\u201320. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76805-0_1"},{"key":"10_CR30","unstructured":"Trajkovska, K., Kljun, M., Pucihar, K.\u010c.: Gaze2AOI: open source deep-learning based system for automatic area of interest annotation with eye tracking data. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR31","unstructured":"Weber, T.: Explainability for embedding AI: aspirations and actuality. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"},{"key":"10_CR32","series-title":"Human\u2013Computer Interaction Series","doi-asserted-by":"publisher","first-page":"E1","DOI":"10.1007\/978-3-319-51838-1_21","volume-title":"The Handbook of Formal Methods in Human-Computer Interaction","author":"B Weyers","year":"2017","unstructured":"Weyers, B., Bowen, J., Dix, A., Palanque, P.: Erratum to: the handbook of formal methods in human-computer interaction. In: Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds.) The Handbook of Formal Methods in Human-Computer Interaction. HIS, pp. E1\u2013E3. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-51838-1_21"},{"key":"10_CR33","unstructured":"Ziegler, J.: Challenges in integrating conversational AI and GUI-based applications. In: Engineering Interactive Systems Embedding AI Technologies Workshop, Cagliary, Sardinia, Italy, June 2024"}],"container-title":["Lecture Notes in Computer Science","Engineering Interactive Computer Systems. EICS 2024 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91760-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T16:57:51Z","timestamp":1748537871000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91760-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031917592","9783031917608"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91760-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"EICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Engineering Interactive Computer Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cagliari","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"eics2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/eics.acm.org\/2024\/workshop-list.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}