{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:40:00Z","timestamp":1780116000319,"version":"3.54.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030915490","type":"print"},{"value":"9783030915506","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91550-6_4","type":"book-chapter","created":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T20:00:31Z","timestamp":1637697631000},"page":"43-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Increasing Engagement with Interactive Visualization: Formal Methods as Serious Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-3142","authenticated-orcid":false,"given":"Lukas","family":"Gr\u00e4tz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,11,23]]},"reference":[{"key":"4_CR1","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"3","key":"4_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s40869-019-00080-6","volume":"8","author":"J Arjoranta","year":"2019","unstructured":"Arjoranta, J.: How to define games and why we need to. Comput. Games J. 8(3), 109\u2013120 (2019). https:\/\/doi.org\/10.1007\/s40869-019-00080-6","journal-title":"Comput. Games J."},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-61511-3_84","volume-title":"Automated Deduction \u2014 Cade-13","author":"M Baaz","year":"1996","unstructured":"Baaz, M., Ferm\u00fcller, C.G., Salzer, G., Zach, R.: MUltlog 1.0: towards an expert system for many-valued logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 226\u2013230. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_84"},{"key":"4_CR4","unstructured":"Baecker, R. Sorting out sorting. Educational film (1980)"},{"key":"4_CR5","unstructured":"Baecker, R.: Sorting out sorting: a case study of software visualization for teaching computer science. In: Software Visualization: Programming as a Multimedia Experience, pp. 369\u2013382 (1998)"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Cerone, A., Roggenbach, M. (eds.) Formal Methods - Fun for Everybody, Revised Selected Papers. CCIS, vol. 1301. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-71374-4","DOI":"10.1007\/978-3-030-71374-4"},{"key":"4_CR7","unstructured":"Cerone, A., et al.: Rooting formal methods within higher education curricula for computer science and software engineering - a white paper. White paper (2020). https:\/\/arxiv.org\/abs\/2010.05708"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/3-540-68716-5_69","volume-title":"Intelligent Tutoring Systems","author":"M D\u2019Agostino","year":"1998","unstructured":"D\u2019Agostino, M., Mondadori, M., Endriss, U., Gabbay, D., Pitt, J.: WinKE: a pedagogic tool for teaching logic and reasoning. In: Goettl, B.P., Halff, H.M., Redfield, C.L., Shute, V.J. (eds.) ITS 1998. LNCS, vol. 1452, p. 605. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-68716-5_69"},{"key":"4_CR9","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32441-4","volume-title":"Formal Methods Teaching","year":"2019","unstructured":"Dongol, B., Petre, L., Smith, G. (eds.): Formal Methods Teaching. LNCS, vol. 11758. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-32441-4"},{"key":"4_CR10","unstructured":"Ehle, A., Hundeshagen, N., Lange, M.: The sequent calculus trainer - helping students to correctly construct proofs. In: 4th International Conference on Tools for Teaching Logic TTL. abs\/1507.03666 (2015)"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Ehle, A., Hundeshagen, N., Lange, M.: The sequent calculus trainer with automated reasoning - helping students to find proofs. In: Quaresma, P., Neuper, W. (eds.) 6th International Workshop on Theorem Proving Components for Educational Software. EPTCS, vol. 267pp. 19\u201337 (2017). https:\/\/doi.org\/10.4204\/EPTCS.267.2","DOI":"10.4204\/EPTCS.267.2"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-48754-9_26","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Endriss","year":"1999","unstructured":"Endriss, U.: An interactive theorem proving assistant. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 308\u2013313. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48754-9_26"},{"key":"4_CR13","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-030-71374-4_11","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"M Farrell","year":"2021","unstructured":"Farrell, M., Wu, H.: When the student becomes the teacher. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 208\u2013217. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_11"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-7643-8354-1_2","volume-title":"Logica Universalis","author":"M Garc\u00eda-Matos","year":"2007","unstructured":"Garc\u00eda-Matos, M., V\u00e4\u00e4n\u00e4nen, J.: Abstract model theory as a framework for universal logic. In: Beziau, J.-Y. (ed.) Logica Universalis, pp. 19\u201333. Birkh\u00e4user, Basel (2007)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-21350-2_11","volume-title":"Tools for Teaching Logic","author":"O Gasquet","year":"2011","unstructured":"Gasquet, O., Schwarzentruber, F., Strecker, M.: Panda: a proof assistant in natural deduction for all. A Gentzen style proof assistant for undergraduate students. In: Blackburn, P., van Ditmarsch, H., Manzano, M., Soler-Toscano, F. (eds.) TICTTL 2011. LNCS (LNAI), vol. 6680, pp. 85\u201392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21350-2_11"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Gual\u00e0, L., Leucci, S., Natale, E.: Bejeweled, candy crush and other match-three games are (NP-)hard. In: IEEE CIG, pp. 1\u20138. IEEE (2014). https:\/\/doi.org\/10.1109\/CIG.2014.6932866","DOI":"10.1109\/CIG.2014.6932866"},{"key":"4_CR17","unstructured":"Hjelsvold, R., Nykvist, S. S., Lor\u00e5s, M., Bahmani, A., Krokan, A.: Educators\u2019 experiences online: how COVID-19 encouraged pedagogical change in CS education. In: Norwegian Conference on Didactics in IT education (2020)"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Hundhausen, C.D.: Toward effective algorithm visualization artifacts: designing for participation and negotiation in an undergraduate algorithms course. In: Karat, C., Lund, A. M. (eds.) CHI, pp. 54\u201355. ACM (1998). https:\/\/doi.org\/10.1145\/286498.286526","DOI":"10.1145\/286498.286526"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1006\/jvlc.2002.0237","volume":"13","author":"CD Hundhausen","year":"2002","unstructured":"Hundhausen, C.D., Douglas, S.A., Stasko, J.T.: A meta-study of algorithm visualization effectiveness. J. Vis. Lang. Comput. 13(3), 259\u2013290 (2002). https:\/\/doi.org\/10.1006\/jvlc.2002.0237","journal-title":"J. Vis. Lang. Comput."},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"100581","DOI":"10.1016\/j.jlamp.2020.100581","volume":"117","author":"W Kahl","year":"2020","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in the teaching tool CalcCheck. J. Log. Algebraic Methods Program. 117, 100581 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100581","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"6","key":"4_CR21","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1177\/1046878114563660","volume":"45","author":"RN Landers","year":"2014","unstructured":"Landers, R.N.: Developing a theory of gamified learning: linking serious games and gamification of learning. Simul. Gaming 45(6), 752\u2013768 (2014). https:\/\/doi.org\/10.1177\/1046878114563660","journal-title":"Simul. Gaming"},{"key":"4_CR22","unstructured":"Materzok, M.: Easyprove: a tool for teaching precise reasoning. In: 4th International Conference on Tools for Teaching Logic TTL. abs\/1507.03675 (2015)"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Myller, N., Bednarik, R., Sutinen, E., Ben-Ari, M. Extending the engagement taxonomy: software visualization and collaborative learning. ACM Trans. Comput. Educ. 9(1), 7:1\u20137:27 (2009). https:\/\/doi.org\/10.1145\/1513593.1513600","DOI":"10.1145\/1513593.1513600"},{"issue":"2","key":"4_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/782941.782998","volume":"35","author":"TL Naps","year":"2003","unstructured":"Naps, T.L., et al.: Exploring the role of visualization and engagement in computer science education. ACM SIGCSE Bull. 35(2), 131\u2013152 (2003). https:\/\/doi.org\/10.1145\/782941.782998","journal-title":"ACM SIGCSE Bull."},{"key":"4_CR25","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-71374-4_3","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"PC \u00d6lveczky","year":"2021","unstructured":"\u00d6lveczky, P.C.: Teaching formal methods for fun using maude. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 58\u201391. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_3"},{"key":"4_CR26","unstructured":"Pierce, B.C., et al.: Software foundations (2021). https:\/\/softwarefoundations.cis.upenn.edu\/lf-current\/index.html"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Prasetya, W., et al.: Having fun in learning formal specifications. In: ICSE-SEET, pp. 192\u2013196 (2019). https:\/\/doi.org\/10.1109\/ICSE-SEET.2019.00028","DOI":"10.1109\/ICSE-SEET.2019.00028"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1037\/h0033456","volume":"19","author":"FC Richardson","year":"1972","unstructured":"Richardson, F.C., Suinn, R.M.: The mathematics anxiety rating scale: psychometric data. J. Couns. Psychol. 19(6), 551\u2013554 (1972). https:\/\/doi.org\/10.1037\/h0033456","journal-title":"J. Couns. Psychol."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Roggenbach, M., Cerone, A., Schlingloff, H., Schneider, G., Shaikh, S.A.: Formal Methods for Software Engineering. Springer (2022, to appear). https:\/\/link.springer.com\/book\/9783030387990","DOI":"10.1007\/978-3-030-38800-3"},{"key":"4_CR30","unstructured":"Smullyan, R.: The riddle of Scheherazade and other amazing puzzles, ancient & modern. New York (1997)"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Spichkova, M., Zamansky, A.: Teaching of formal methods for software engineering. In: Maciaszek, L.A., Filipe, J. (eds.) ENASE, pp. 370\u2013376. SciTePress (2016). https:\/\/doi.org\/10.5220\/0005928503700376","DOI":"10.5220\/0005928503700376"},{"issue":"2","key":"4_CR32","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1037\/a0031311","volume":"105","author":"P Wouters","year":"2013","unstructured":"Wouters, P., van Nimwegen, C., van Oostendorp, H., van der Spek, E.D.: A meta-analysis of the cognitive and motivational effects of serious games. J. Educ. Psychol. 105(2), 249\u2013265 (2013). https:\/\/doi.org\/10.1037\/a0031311","journal-title":"J. Educ. Psychol."},{"key":"4_CR33","unstructured":"Zach, R.: Boxes and diamonds: an open introduction to modal logic (2019)"},{"key":"4_CR34","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-030-71374-4_12","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"R Zhumagambetov","year":"2021","unstructured":"Zhumagambetov, R.: Teaching formal methods in academia: a systematic literature review. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 218\u2013226. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_12"}],"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-030-91550-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T02:57:17Z","timestamp":1673837837000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91550-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030915490","9783030915506"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91550-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 November 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfm2021","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"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}