{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T17:17:31Z","timestamp":1794503851244,"version":"4.9.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319231648","type":"print"},{"value":"9783319231655","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_21","type":"book-chapter","created":{"date-parts":[[2015,8,25]],"date-time":"2015-08-25T23:57:43Z","timestamp":1440547063000},"page":"451-474","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Reachability-Logic Properties on Rewriting-Logic Specifications"],"prefix":"10.1007","author":[{"given":"Dorel","family":"Lucanu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Arusoaie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"issue":"1","key":"21_CR1","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). Selected Papers of the 2nd Workshop on Concurrency and Compositionality","journal-title":"Theor. Comput. Sci."},{"key":"21_CR2","volume-title":"All about Maude - A High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","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: How to Specify, Program and Verify Systems in Rewriting Logic. Springer, Heidelberg (2007)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Checking reachability using matching logic. In: Leavens, G.T., Dwyer, M.B. (eds) OOPSLA, pp. 555\u2013574. ACM (2012). also available as technical report http:\/\/hdl.handle.net\/2142\/33771","DOI":"10.1145\/2398857.2384656"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-642-31585-5_33","volume-title":"Automata, Languages, and Programming","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Towards a unified theory of operational and Axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 351\u2013363. Springer, Heidelberg (2012)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Symposium on Logic in Computer Science (LICS 2013), pp. 358\u2013367. IEEE, June 2013","DOI":"10.1109\/LICS.2013.42"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Mereuta, R., Moore, B.M., \u015eerb\u0103nut\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Heidelberg (2014)"},{"issue":"3","key":"21_CR7","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":"21_CR8","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":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bogd\u0103na\u015f, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. In Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL 2015), pp. 445\u2013456. ACM, January 2015","DOI":"10.1145\/2676726.2676982"},{"issue":"6","key":"21_CR10","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."},{"issue":"7","key":"21_CR11","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), 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/S1571-0661(05)82534-4","volume":"71","author":"S Eker","year":"2004","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. Electron. Notes Theor. Comput. Sci. 71, 162\u2013187 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"21_CR14","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: 24th International Conference on Rewriting Techniques and Applications, RTA 2013, 24\u201326 June 2013, pp. 81\u201396, Eindhoven, The Netherlands (2013)"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-22944-2_22","volume-title":"Algebra and Coalgebra in Computer Science","author":"C Rocha","year":"2011","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314\u2013328. Springer, Heidelberg (2011)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-13977-2_12","volume-title":"Tests and Proofs","author":"V Rusu","year":"2010","unstructured":"Rusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 135\u2013150. Springer, Heidelberg (2010)"},{"issue":"1","key":"21_CR17","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"21_CR18","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. Theor. Comput. Sci. 403(2), 239\u2013264 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"21_CR19","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.jlap.2009.07.003","volume":"79","author":"J Meseguer","year":"2009","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Algebraic simulations. J. Logic Algebraic Program. 79(2), 103\u2013143 (2009)","journal-title":"J. Logic Algebraic Program."},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-319-02654-1_16","volume-title":"Software Language Engineering","author":"A Arusoaie","year":"2013","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 281\u2013301. Springer, Heidelberg (2013). http:\/\/hal.inria.fr\/hal-00853588"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-319-12904-4_14","volume-title":"Rewriting Logic and Its Applications","author":"C Rocha","year":"2014","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 247\u2013262. Springer, Heidelberg (2014)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-319-12904-4_5","volume-title":"Rewriting Logic and Its Applications","author":"A Arusoaie","year":"2014","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V., \u015eerb\u0103nu\u0163\u0103, T.-F., \u015etef\u0103nescu, A., Ro\u015fu, G.: Language definitions as rewrite theories. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 97\u2013112. Springer, Heidelberg (2014)"},{"key":"21_CR23","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana Champaign (2008)"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T13:06:54Z","timestamp":1675256814000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}