{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:57Z","timestamp":1740099057887,"version":"3.37.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-90686-7_13","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:49:55Z","timestamp":1524491395000},"page":"198-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Parameterized by\u00a0the\u00a0Semantics in Maude"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-4612","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Riesco","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-22438-6_5","volume-title":"Automated Deduction \u2013 CADE-23","author":"M Alpuente","year":"2011","unstructured":"Alpuente, M., Ballis, D., Espert, J., Romero, D.: Backward trace slicing for rewriting logic theories. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 34\u201348. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22438-6_5"},{"key":"13_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-770-1","volume-title":"Principles of the Spin Model Checker","author":"M Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the Spin Model Checker. Springer, London (2008). \nhttps:\/\/doi.org\/10.1007\/978-1-84628-770-1"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236, 35\u2013132 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"13_CR5","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/j.scico.2016.11.002","volume":"147","author":"E Angelis De","year":"2017","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions via program specialization. Sci. Comput. Program. 147, 78\u2013108 (2017)","journal-title":"Sci. Comput. Program."},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-24933-4_17","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"F Dur\u00e1n","year":"2011","unstructured":"Dur\u00e1n, F., Rocha, C., \u00c1lvarez, J.M.: Towards a Maude formal environment. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 329\u2013351. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24933-4_17"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages, POPL 2012, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501\u2013505. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_46"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11784180_13","volume-title":"Algebraic Methodology and Software Technology","author":"A Farzan","year":"2006","unstructured":"Farzan, A., Meseguer, J.: State space reduction of rewrite theories using invisible transitions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 142\u2013157. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11784180_13"},{"issue":"4\u20136","key":"13_CR12","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1017\/S1471068410000347","volume":"10","author":"M G\u00f3mez-Zamalloa","year":"2010","unstructured":"G\u00f3mez-Zamalloa, M., Albert, E., Puebla, G.: Test case generation for object-oriented imperative languages in CLP. Theor. Pract. Log. Program. 10(4\u20136), 659\u2013674 (2010)","journal-title":"Theor. Pract. Log. Program."},{"issue":"4","key":"13_CR13","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"13_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(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"13_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., Ro\u015fu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-662-54494-5_21","volume-title":"Fundamental Approaches to Software Engineering","author":"A Riesco","year":"2017","unstructured":"Riesco, A., As\u0103voae, I.M., As\u0103voae, M.: Slicing from formal semantics: Chisel. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 374\u2013378. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54494-5_21"},{"issue":"6","key":"13_CR17","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. Log. Algebr. Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"13_CR18","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.jlamp.2015.09.001","volume":"85","author":"V Rusu","year":"2016","unstructured":"Rusu, V., Lucanu, D., Serbanuta, T., Arusoaie, A., Stefanescu, A., Ro\u015fu, G.: Language definitions as rewrite theories. J. Log. Algebraic Methods Program. 85(1), 98\u2013120 (2016)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1016\/j.jlap.2005.09.008","volume":"67","author":"A Verdejo","year":"2006","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Executable structural operational semantics in Maude. J. Log. Algebr. Program. 67, 226\u2013293 (2006)","journal-title":"J. Log. Algebr. Program."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:53:48Z","timestamp":1524491628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}