{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:38Z","timestamp":1785202238751,"version":"3.55.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_16","type":"book-chapter","created":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T14:13:51Z","timestamp":1749392031000},"page":"275-293","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Algorithmic Analysis of\u00a0Event-B in\u00a0Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Olarte","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Osorio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlos","family":"Ram\u00edrez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"16_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J Abrial","year":"2010","unstructured":"Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"16_CR3","first-page":"213","volume":"153","author":"G Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. ENTCS 153(2), 213\u2013239 (2006)","journal-title":"ENTCS"},{"key":"16_CR4","doi-asserted-by":"publisher","DOI":"10.1145\/3019612.3019823","author":"M Amine","year":"2017","unstructured":"Amine, M., Delahaye, B., Lanoix, A.: Moving from Event-B to probabilistic Event-B. Tech. Rep. (2017). https:\/\/doi.org\/10.1145\/3019612.3019823","journal-title":"Tech. Rep."},{"key":"16_CR5","unstructured":"Aouadhi, M.A., Delahaye, B., Lanoix, A.: A Fully Probabilistic Extension of Event-B. Research report, LINA-University of Nantes (2016)"},{"issue":"3","key":"16_CR6","doi-asserted-by":"publisher","first-page":"1953","DOI":"10.1007\/s10270-017-0626-5","volume":"18","author":"MA Aouadhi","year":"2019","unstructured":"Aouadhi, M.A., Delahaye, B., Lanoix, A.: Introducing probabilistic reasoning within Event-B. Softw. Syst. Model. 18(3), 1953\u20131984 (2019)","journal-title":"Softw. Syst. Model."},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10009-016-0431-4","volume":"19","author":"F Boniol","year":"2017","unstructured":"Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.: The landing gear case study: challenges and experiments. Int. J. Softw. Tools Technol. Transf. 19(2), 133\u2013140 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR8","unstructured":"Braga, C., Mart\u00ed-Oliet, N.: B Maude: a formal executable environment for abstract machine notation descriptions. CoRR abs\/2108.07878 (2021)"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"100497","DOI":"10.1016\/j.jlamp.2019.100497","volume":"110","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"5","key":"16_CR11","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"OOPSLA2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1145\/3563299","volume":"6","author":"S Liu","year":"2022","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.A.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022)","journal-title":"Proc. ACM Program. Lang."},{"issue":"1","key":"16_CR13","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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"7\u20138","key":"16_CR14","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"16_CR15","unstructured":"Olarte, C., Osorio, D., Ram\u00edrez, C., Rocha, C.: EventB2Maude. https:\/\/github.com\/carlosolarte\/EventB2Maude (2025)"},{"issue":"8","key":"16_CR16","doi-asserted-by":"publisher","first-page":"2240","DOI":"10.1093\/logcom\/exab062","volume":"31","author":"MY Pedersen","year":"2021","unstructured":"Pedersen, M.Y., Smets, S., \u00c5gotnes, T.: Modal logics and group polarization. J. Log. Comput. 31(8), 2240\u20132269 (2021)","journal-title":"J. Log. Comput."},{"issue":"1","key":"16_CR17","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Logical Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"100700","DOI":"10.1016\/j.jlamp.2021.100700","volume":"123","author":"R Rubio","year":"2021","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebraic Methods Program. 123, 100700 (2021)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"16_CR19","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horv\u00e1th, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) ValueTools\u201913, Torino, pp. 310\u2013315. ICST\/ACM (2013)"},{"issue":"1","key":"16_CR20","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s00165-014-0305-z","volume":"27","author":"A Tarasyuk","year":"2015","unstructured":"Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Integrating stochastic reasoning into Event-B development. Formal Aspects Comput. 27(1), 53\u201377 (2015)","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93706-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T14:13:54Z","timestamp":1749392034000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}