{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T05:10:18Z","timestamp":1746508218640,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031124402"},{"type":"electronic","value":"9783031124419"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-12441-9_5","type":"book-chapter","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:34Z","timestamp":1659090214000},"page":"85-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Teaching Formal Methods to\u00a0Undergraduate Students Using Maude"],"prefix":"10.1007","author":[{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,30]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-04912-5_11","volume-title":"Teaching Formal Methods","author":"L Aceto","year":"2009","unstructured":"Aceto, L., Ingolfsdottir, A., Larsen, K.G., Srba, J.: Teaching concurrency: theory in practice. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 158\u2013175. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04912-5_11"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"GA Agha","year":"2006","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_28"},{"issue":"3","key":"5_CR4","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"DA Basin","year":"2022","unstructured":"Basin, D.A., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20(3), 24\u201332 (2022)","journal-title":"IEEE Secur. Priv."},{"key":"5_CR5","unstructured":"Basin, D.A., Sasse, R., Toro-Pozo, J.: Card brand mixup attack: bypassing the PIN in non-Visa cards by using them for Visa transactions. In: 30th USENIX Security Symposium, USENIX Security 2021, pp. 179\u2013194. USENIX Association (2021)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Sasse, R., Toro-Pozo, J.: The EMV standard: break, fix, verify. In: 42nd IEEE Symposium on Security and Privacy, SP 2021. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00037"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Bobba, R., et al.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. In: Assured Cloud Computing, chap. 2, pp. 10\u201348. Wiley-IEEE Computer Society Press (2018)","DOI":"10.1002\/9781119428497.ch2"},{"key":"5_CR8","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-71374-4_1","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"A Cerone","year":"2021","unstructured":"Cerone, A., et al.: Rooting formal methods within higher education curricula for computer science and software engineering: a white paper. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 1\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_1"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Chen, S., Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.M.: A systematic approach to uncover security flaws in GUI logic. In: IEEE Symposium on Security and Privacy, pp. 71\u201385. IEEE Computer Society (2007)","DOI":"10.1109\/SP.2007.6"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C.A., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"5_CR12","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-030-71374-4_6","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"S Krings","year":"2021","unstructured":"Krings, S., K\u00f6rner, P.: Prototyping games using formal methods. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 124\u2013142. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_6"},{"issue":"2","key":"5_CR13","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1595453.1595457","volume":"41","author":"S Liu","year":"2009","unstructured":"Liu, S., Takahashi, K., Hayashi, T., Nakayama, T.: Teaching formal methods in the context of software engineering. ACM SIGCSE Bull. 41(2), 17\u201323 (2009)","journal-title":"ACM SIGCSE Bull."},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96, 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.08.004","volume":"231","author":"J Meseguer","year":"2013","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project: a progress report. Inf. Comput. 231, 38\u201369 (2013)","journal-title":"Inf. Comput."},{"issue":"4","key":"5_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","journal-title":"Commun. ACM"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Rewriting Logic and Its Applications","author":"PC \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3"},{"key":"5_CR19","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":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"key":"5_CR21","series-title":"Undergraduate Topics in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-6687-0","volume-title":"Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude","author":"PC \u00d6lveczky","year":"2017","unstructured":"\u00d6lveczky, P.C.: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. UTCS, Springer, London (2017). https:\/\/doi.org\/10.1007\/978-1-4471-6687-0"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Ro\u015fu, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the ESEC\/FSE 2018, pp. 912\u2013915. ACM (2018)","DOI":"10.1145\/3236024.3264591"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Peltonen, A., Sasse, R., Basin, D.A.: A comprehensive formal analysis of 5G handover. In: 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec 2021, pp. 1\u201312. ACM (2021)","DOI":"10.1145\/3448300.3467823"},{"issue":"6","key":"5_CR24","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"5_CR25","unstructured":"Schwartz, D.G.: Rethinking the CS curriculum. Blog at the Communications of the ACM, May 2022. https:\/\/cacm.acm.org\/blogs\/blog-cacm\/261380-rethinking-the-cs-curriculum\/fulltext"},{"key":"5_CR26","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: ValueTools, pp. 310\u2013315. ICST\/ACM (2013)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MY Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1\u201322. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_1"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-12441-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:51Z","timestamp":1659090231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-12441-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031124402","9783031124419"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-12441-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sv.postech.ac.kr\/wrla2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}