{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:06:32Z","timestamp":1771045592184,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","funder":[{"name":"NASA University Leadership Initiative grant (ULI)","award":["80NSSC22M0070"],"award-info":[{"award-number":["80NSSC22M0070"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,13]]},"DOI":"10.1145\/3724363.3729116","type":"proceedings-article","created":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T08:57:23Z","timestamp":1750150643000},"page":"187-193","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["'Too Theoretical and Nowhere Near Interesting': Using a Tool to Increase Student Motivation for Formal Methods"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9838-8028","authenticated-orcid":false,"given":"Katherine","family":"Braught","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4633-9408","authenticated-orcid":false,"given":"Yangge","family":"Li","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3760-9859","authenticated-orcid":false,"given":"Katherine","family":"Driggs-Campbell","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6672-8470","authenticated-orcid":false,"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--57663--9_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-08-097086--8.26099--6"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113792.1113794"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595453.1595459"},{"key":"e_1_3_2_1_5_1","unstructured":"Hugo Brakman Vincent Driessen Joseph Kavuma B Nij Bijvank and Sander Vermolen. 2006. Supporting Formal Methods Teaching with Real-Life Protocols. (2006)."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--71374--4_1"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","volume-title":"All about maude-A high-performance logical framework how to specify, program and verify systems in rewriting logic","author":"Clavel Manuel","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007. All about maude-A high-performance logical framework how to specify, program and verify systems in rewriting logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 4350. 1--819."},{"key":"e_1_3_2_1_8_1","volume-title":"Fun with Formal Methods: Workshop at the 25th International Conference on Computer Aided Verification. Citeseer.","author":"Curzon Paul","year":"2013","unstructured":"Paul Curzon and Peter W McOwan. 2013. Teaching formal methods using magic tricks. In Fun with Formal Methods: Workshop at the 25th International Conference on Computer Aided Verification. Citeseer."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71374-4_8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Norman T. Feather (Ed.). 2021. Expectations and Actions: Expectancy-Value Models in Psychology. Routledge London. https:\/\/doi.org\/10.4324\/9781003150879","DOI":"10.4324\/9781003150879"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--58298--2_1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPSW.2012.164"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.149.4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--91550--6_4"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1177\/0272431614556890"},{"key":"e_1_3_2_1_16_1","volume-title":"Verse: A Python Library for\u00a0Reasoning About Multi-agent Hybrid System Scenarios","author":"Li Yangge","year":"2023","unstructured":"Yangge Li, Haoqing Zhu, Katherine Braught, Keyi Shen, and Sayan Mitra. 2023. Verse: A Python Library for\u00a0Reasoning About Multi-agent Hybrid System Scenarios. In Computer Aided Verification, Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland, Cham, 351--364."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595453.1595457"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04912-5_3"},{"key":"e_1_3_2_1_19_1","volume-title":"2019 IEEE\/ACM 41st International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET). IEEE, 192--196","author":"Prasetya Wishnu","unstructured":"Wishnu Prasetya, Craig Leek, Orestis Melkonian, Joris ten Tusscher, Jan van Bergen, Jasper Everink, Thomas van der Klis, Rick Meijerink, Roan Oosenbrug, Jelle Oostveen, et al. 2019. Having fun in learning formal specifications. In 2019 IEEE\/ACM 41st International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET). IEEE, 192--196."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1541-0420.2005.00389.x"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71374-4_7"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.15388\/infedu.2022.04"},{"key":"e_1_3_2_1_23_1","volume-title":"Teaching Formal Methods in Computer Science Undergraduates. (Jan","author":"Sotiriadou Anna","year":"2000","unstructured":"Anna Sotiriadou and Petros Kefalas. 2000. Teaching Formal Methods in Computer Science Undergraduates. (Jan. 2000)."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3702231"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.223"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71374-4_12"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--71374--4_3"}],"event":{"name":"ITiCSE 2025: Innovation and Technology in Computer Science Education","location":"Nijmegen Netherlands","acronym":"ITiCSE 2025","sponsor":["SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 30th ACM Conference on Innovation and Technology in Computer Science Education V. 1"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3724363.3729116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T15:22:33Z","timestamp":1765207353000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3724363.3729116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,13]]},"references-count":27,"alternative-id":["10.1145\/3724363.3729116","10.1145\/3724363"],"URL":"https:\/\/doi.org\/10.1145\/3724363.3729116","relation":{},"subject":[],"published":{"date-parts":[[2025,6,13]]},"assertion":[{"value":"2025-06-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}