{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T02:29:35Z","timestamp":1768271375069,"version":"3.49.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319944593","type":"print"},{"value":"9783319944609","type":"electronic"}],"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-94460-9_12","type":"book-chapter","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:36:38Z","timestamp":1531136198000},"page":"201-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Constructor-Based Reachability Logic for Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Stephen","family":"Skeirik","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Stefanescu","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,10]]},"reference":[{"key":"12_CR1","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: How to Specify, Program and Verify Systems in Rewriting Logic","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: 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":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"12_CR3","first-page":"243","volume-title":"Formal Models and Semantics","author":"Nachum DERSHOWITZ","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. North-Holland (1990)"},{"issue":"7\u20138","key":"12_CR4","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program. 81(7\u20138), 816\u2013850 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-16901-4_1","volume-title":"Formal Methods and Software Engineering","author":"K Futatsugi","year":"2010","unstructured":"Futatsugi, K.: Fostering proof scores in CafeOBJ. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 1\u201320. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16901-4_1"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-319-23165-5_21","volume-title":"Logic, Rewriting, and Concurrency: Essays dedicated to Jos\u00e9 Meseguer on the Occasion of His 65th Birthday","author":"D Lucanu","year":"2015","unstructured":"Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 451\u2013474. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23165-5_21"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","volume":"85","author":"S Lucas","year":"2016","unstructured":"Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Meth. Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"12_CR8","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. Algebr. Logic Program. 81, 721\u2013781 (2012)","journal-title":"J. Algebr. Logic Program."},{"key":"12_CR9","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-29510-7_1","volume-title":"Formal Techniques for Safety-Critical Systems","author":"J Meseguer","year":"2016","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 3\u201334. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-29510-7_1"},{"key":"12_CR10","unstructured":"Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Algebraic Methods in Semantics, pp. 459\u2013541. Cambridge UP (1985)"},{"key":"12_CR11","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. Logic Algebr. Methods Program. 86, 269\u2013297 (2017)","journal-title":"J. Logic Algebr. Methods Program."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-44802-2_10","volume-title":"Rewriting Logic and Its Applications","author":"S Skeirik","year":"2016","unstructured":"Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 167\u2013184. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-44802-2_10"},{"key":"12_CR13","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Technical report. \nhttp:\/\/hdl.handle.net\/2142\/95770"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., et al.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08918-8_29"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the OOPSLA 2016, pp. 74\u201391. ACM (2016)","DOI":"10.1145\/2983990.2984027"},{"issue":"1\u20132","key":"12_CR16","first-page":"123","volume":"20","author":"P Thati","year":"2007","unstructured":"Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. High.-Order Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. High.-Order Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94460-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:44:19Z","timestamp":1531136659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94460-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944593","9783319944609"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94460-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}