{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:21:45Z","timestamp":1743157305721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031659409"},{"type":"electronic","value":"9783031659416"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-65941-6_11","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"195-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Teaching an Advanced Maude-Based Formal Methods Course in Oslo"],"prefix":"10.1007","author":[{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Teaching concurrency: Theory in practice. In: Proceedings of Teaching Formal Methods 2009. LNCS, vol.\u00a05846. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04912-5_11"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2) (2006)","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model checking and quantitative analysis tool. In: CALCO\u201911, LNCS, vol.\u00a06859. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22944-2_28"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Lectures on Runtime Verification: Introductory and Advanced Topics, LNCS, vol. 10457, pp. 1\u201333. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-75632-5_1"},{"issue":"3","key":"11_CR5","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":"11_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":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bentea, L., \u00d6lveczky, P.C., Bentea, E.: Using probabilistic strategies to formalize and compare $$\\alpha $$-synuclein aggregation and propagation under different scenarios. In: Proceedings of Computational Methods in Systems Biology (CMSB\u201913). LNCS, vol.\u00a08130. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40708-6_8"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., \u00d6lveczky, P.C., Skeirik, S.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. In: Assured Cloud Computing, Chap.\u00a02, pp. 10\u201348. Wiley-IEEE Computer Society Press (2018)","DOI":"10.1002\/9781119428497.ch2"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Cerone, A., et\u00a0al.: Rooting formal methods within higher education curricula for computer science and software engineering: A white paper. In: Proceedings of FMfun 2019, First International Workshop on Formal Methods\u2014Fun for Everybody. Communications in Computer and Information Science (CCIS), vol.\u00a01301. Springer, Berlin (2020)","DOI":"10.1007\/978-3-030-71374-4_1"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Chen, X., Rosu, G.: The K vision for the future of programming language design and analysis. In: Formal Methods in Outer Space: Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, vol. 13065, pp.\u00a03\u20139. Springer, Berlin (2021)","DOI":"10.1007\/978-3-030-87348-6_1"},{"key":"11_CR11","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Maude Manual (Version 3.3.1) (2023). http:\/\/maude.cs.illinois.edu"},{"key":"11_CR12","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude, LNCS, vol.\u00a04350. Springer, Berlin (2007)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.L.: Pathway logic: Executable models of biological networks. In: Proceedings of WRLA 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a071, pp. 144\u2013161. Elsevier (2002)","DOI":"10.1016\/S1571-0661(05)82533-2"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"11_CR15","unstructured":"Garcia-Luna-Aceves, J., Zhang, Y.: Reliable broadcasting in dynamic networks. In: Proceedings of IEEE ICC. IEEE (1996)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A complete formal semantics of the ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, pp. 204\u2013217. IEEE Computer Society (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"11_CR17","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."},{"key":"11_CR18","unstructured":"Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.: A systematic approach to uncover security flaws in GUI logic. In: 2007 IEEE Symposium on Security and Privacy (S &P 2007). IEEE Computer Society (2007)"},{"issue":"4","key":"11_CR19","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":"11_CR20","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Semantics, simulation, and formal analysis of modeling languages for embedded systems in Real-Time Maude. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Talcott Festschrift, Lecture Notes in Computer Science, vol.\u00a07000, pp. 368\u2013402. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24933-4_19"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: WRLA 2014. LNCS, vol.\u00a08663. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Teaching formal methods for fun using Maude. In: Proceedings of FMfun 2019, First International Workshop on Formal Methods\u2014Fun for Everybody. Communications in Computer and Information Science (CCIS), vol.\u00a01301, pp. 58\u201391. Springer, Berlin (2020)","DOI":"10.1007\/978-3-030-71374-4_3"},{"issue":"1\u20132","key":"11_CR23","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order Symbolic Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"Higher-Order Symbolic Comput."},{"key":"11_CR24","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: Proceedings of TACAS\u201908. LNCS, vol.\u00a04963. Springer, Berlin (2008)"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Formalizing and validating the P-Store replicated data store in Maude. In: Proceedings of WADT\u201916. LNCS, vol. 10644. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-72044-9_13"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Undergraduate Topics in Computer Science. Springer, Berlin (2017)","DOI":"10.1007\/978-1-4471-6687-0"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Teaching formal methods to undergraduate students using Maude. In: Rewriting Logic and Its Applications (WRLA@ETAPS 2022). LNCS, vol. 13252. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-12441-9_5"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Roggenbach, M., Cerone, A., Schlingloff, B., Schneider, G., Shaikh, S.A.: Formal Methods for Software Engineering: Languages, Methods, Application Domains. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2022)","DOI":"10.1007\/978-3-030-38800-3"},{"issue":"2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Rosu","year":"2005","unstructured":"Rosu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151\u2013197 (2005)","journal-title":"Autom. Softw. Eng."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Schiper, N., Sutra, P., Pedone, F.: P-Store: Genuine partial replication in wide area networks. In: 29th IEEE Symposium on Reliable Distributed Systems (SRDS 2010), pp. 214\u2013224. IEEE Computer Society (2010)","DOI":"10.1109\/SRDS.2010.32"}],"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-65941-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:13:01Z","timestamp":1722496381000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 August 2024","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wrla2024.gitlab.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}