{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T17:12:33Z","timestamp":1783703553157,"version":"3.55.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032267429","type":"print"},{"value":"9783032267436","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-26743-6_1","type":"book-chapter","created":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T12:48:08Z","timestamp":1779108488000},"page":"3-11","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Teaching Logic with\u00a0Specification Challenges"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,19]]},"reference":[{"issue":"5","key":"1_CR1","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10664-025-10687-1","volume":"30","author":"M Alhanahnah","year":"2025","unstructured":"Alhanahnah, M., Rashedul Hasan, M., Xu, L., Bagheri, H.: An empirical evaluation of pre-trained large language models for repairing declarative formal specifications. Empir. Softw. Eng. 30(5), 149 (2025)","journal-title":"Empir. Softw. Eng."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., de\u00a0Halleux, P., Swamy, N., Leijen, D.: Increasing human-tool interaction via the web. In: 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 49\u201352 (2013)","DOI":"10.1145\/2462029.2462031"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Barros, A., Neto, H., Cunha, A., Macedo, N., Paiva, A.C.: Alloy repair hint generation based on historical data. In: 26th International Symposium on Formal Methods, pp. 104\u2013121. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_8","DOI":"10.1007\/978-3-031-71177-0_8"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Brida, S.G., et al.: BeAFix: an automated repair tool for faulty Alloy models. In: 36th IEEE\/ACM International Conference on Automated Software Engineering, pp. 1213\u20131217. IEEE (2021)","DOI":"10.1109\/ASE51524.2021.9678524"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for Alloy 6. In: 20th International Conference on Software Engineering and Formal Methods, pp. 288\u2013303. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_18","DOI":"10.1007\/978-3-031-17108-6_18"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Couto, R., Campos, J.C., Macedo, N., Cunha, A.: Improving the visualization of Alloy instances. In: 4th Workshop on Formal Integrated Development Environment, pp. 37\u201352 (2018)","DOI":"10.4204\/EPTCS.284.4"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N.: Validating formal specifications with LLM-generated test cases. In: 27th International Symposium on Formal Methods. Springer (2026), to appear","DOI":"10.1007\/978-3-032-26204-2_15"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N., Campos, J.C., Margolis, I., Sousa, E.: Assessing the impact of hints in learning formal specification. In: 46th International Conference on Software Engineering: Software Engineering Education and Training, pp. 151\u2013161 (2024)","DOI":"10.1145\/3639474.3640050"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Cunha, A., Macedo, N., Guimar\u00e3es, T.: Target oriented relational model finding. In: 17th International Conference on Fundamental Approaches to Software Engineering, pp. 17\u201331. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_2","DOI":"10.1007\/978-3-642-54804-8_2"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Dyer, T., Baugh, J.: Sterling: A web-based visualizer for relational modeling languages. In: 8th International Conference on Rigorous State-Based Methods, pp. 99\u2013104. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_7","DOI":"10.1007\/978-3-030-77543-8_7"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez\u00a0Brida, S., et al.: ICEBAR: feedback-driven iterative repair of Alloy specifications. In: 37th IEEE\/ACM International Conference on Automated Software Engineering, pp. 1\u201313 (2022)","DOI":"10.1145\/3551349.3556944"},{"issue":"2","key":"1_CR12","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR13","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2012)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Jackson, D.: The Essence of Software: Why Concepts Matter for Great Design. Princeton University Press (2021)","DOI":"10.1515\/9780691230542"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Jovanovic, A., Sullivan, A.: Right or wrong\u2013understanding how users write software models in Alloy. In: 22nd International Conference on Software Engineering and Formal Methods, pp. 309\u2013327. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-77382-2_18","DOI":"10.1007\/978-3-031-77382-2_18"},{"issue":"3","key":"1_CR16","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"1_CR17","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1007\/s10817-022-09642-2","volume":"66","author":"N Macedo","year":"2022","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A.: Pardinus: a temporal relational model finder. J. Autom. Reason. 66(4), 861\u2013904 (2022)","journal-title":"J. Autom. Reason."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: 24th International Symposium on Foundations of Software Engineering, pp. 373\u2013383 (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Macedo, N., Cunha, A., Paiva, A.C.R.: Alloy4Fun dataset for 2019\/20 (2020). https:\/\/doi.org\/10.5281\/zenodo.4665672","DOI":"10.5281\/zenodo.4665672"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Macedo, N., Cunha, A., Paiva, A.C.R.: Alloy4Fun dataset for 2024\/25 (2025). https:\/\/doi.org\/10.5281\/zenodo.17390557","DOI":"10.5281\/zenodo.17390557"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Macedo, N., et al.: Experiences on teaching Alloy with an automated assessment platform. In: 7th International Conference on Rigorous State-Based Methods, pp. 61\u201377. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_5","DOI":"10.1007\/978-3-030-48077-6_5"},{"key":"1_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2021.102690","volume":"211","author":"N Macedo","year":"2021","unstructured":"Macedo, N., et al.: Experiences on teaching Alloy with an automated assessment platform. Sci. Comput. Program. 211, 102690 (2021)","journal-title":"Sci. Comput. Program."},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: 35th International Conference on Software Engineering, pp. 232\u2013241 (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"1_CR24","unstructured":"Pereira, J.: A web-based social environment for Alloy. Master\u2019s thesis, Universidade do Minho (2016)"},{"key":"1_CR25","unstructured":"Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: Lightweight diagramming for lightweight formal methods: a grounded language design. In: 39th European Conference on Object-Oriented Programming, pp. 26\u20131 (2025)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Prasad, S., Greenman, B., Nelson, T., Wrenn, J., Krishnamurthi, S.: Making hay from wheats: a class sourcing method to identify misconceptions. In: 22nd Koli Calling International Conference on Computing Education Research, pp.\u00a01\u20137 (2022)","DOI":"10.1145\/3564721.3564726"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Tillmann, N., De\u00a0Halleux, J., Xie, T., Bishop, J.: Pex4Fun: teaching and learning computer science via social gaming. In: 25th Conference on Software Engineering Education and Training, pp. 90\u201391. IEEE (2012)","DOI":"10.1109\/CSEET.2012.13"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Arepair: a repair framework for Alloy. In: 41st International Conference on Software Engineering: Companion Proceedings, pp. 103\u2013106. IEEE (2019)","DOI":"10.1109\/ICSE-Companion.2019.00049"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, C., et al.: AlloyMax: bringing maximum satisfaction to relational specifications. In: 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 155\u2013167 (2021)","DOI":"10.1145\/3468264.3468587"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Zheng, G., et al.: ATR: template-based repair for alloy specifications. In: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 666\u2013677 (2022)","DOI":"10.1145\/3533767.3534369"}],"container-title":["Lecture Notes in Computer Science","Formal Methods Teaching"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26743-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T16:13:46Z","timestamp":1783700026000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26743-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032267429","9783032267436"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26743-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"19 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMTea","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Formal Methods Teaching Workshop","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmtea.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}