{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T22:54:40Z","timestamp":1768258480492,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031659409","type":"print"},{"value":"9783031659416","type":"electronic"}],"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_1","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Invariants by\u00a0Deductive Model Checking"],"prefix":"10.1007","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ra\u00fal","family":"L\u00f3pez-Rueda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"1_CR1","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA 2013. LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J.: Infinite-state model checking of LTLR formulas using narrowing. In: Proceedings of WRLA 2014. LNCS, vol.\u00a08663, pp. 113\u2013129. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-12904-4_6"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J.: Predicate abstraction of rewrite theories. In: RTA-TLCA. Lecture Notes in Computer Science, vol.\u00a08560, pp. 61\u201376. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08918-8_5"},{"issue":"5","key":"1_CR4","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"KA Bartlett","year":"1969","unstructured":"Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260\u2013261 (1969)","journal-title":"Commun. ACM"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"1_CR6","unstructured":"Dur\u00e1n, F., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: NuITP alpha 21\u2014an inductive theorem prover for maude equational theories. Available at https:\/\/nuitp.webs.upv.es\/"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Equational unification and matching, and symbolic reachability analysis in Maude 3.2. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning\u201411th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8\u201310, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 529\u2013540. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_31","DOI":"10.1007\/978-3-031-10769-6_31"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Foundations of Security Analysis and Design V, FOSAD 2007\/2008\/2009 Tutorial Lectures, LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Escobar, S., L\u00f3pez-Rueda, R., Sapi\u00f1a, J.: Symbolic analysis by using folding narrowing with irreducibility and SMT constraints. In: Artho, C., \u00d6lveczky, P.C. (eds.) Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2023, Cascais, Portugal, 22 October 2023. pp. 14\u201325. ACM (2023). https:\/\/doi.org\/10.1145\/3623503.3623537","DOI":"10.1145\/3623503.3623537"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Proceedings of RTA. Lecture Notes in Computer Science, vol.\u00a04533, pp. 153\u2013168 (2007)","DOI":"10.1007\/978-3-540-73449-9_13"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Logic Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Futatsugi, K.: Advances of proof scores in CafeOBJ. Sci. Comput. Program. 224, 102893 (2022). https:\/\/doi.org\/10.1016\/J.SCICO.2022.102893","DOI":"10.1016\/J.SCICO.2022.102893"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"1_CR15","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."},{"issue":"1\u20132","key":"1_CR16","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. Higher-Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. Higher-Order Symbolic Comput."},{"issue":"1","key":"1_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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Proceedings of WADT\u201997. pp. 18\u201361. Springer LNCS 1376 (1998)","DOI":"10.1007\/3-540-64299-4_26"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3\u201341 (2018)","journal-title":"Sci. Comput. Program."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) Formal Methods for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19.21, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02884, pp. 170\u2013184. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/978-3-540-39958-2_12","DOI":"10.1007\/978-3-540-39958-2_12"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS\/CafeOBJ method. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) Proceedings of the BCS-FACS Refinement Workshop, REFINE@IFM 2007, Oxford, UK, July 2007. Electronic Notes in Theoretical Computer Science, vol.\u00a0201, pp. 127\u2013154. Elsevier (2007). https:\/\/doi.org\/10.1016\/J.ENTCS.2008.02.018","DOI":"10.1016\/J.ENTCS.2008.02.018"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Ogata, K., Futatsugi, K.: Theorem proving based on proof scores for rewrite theory specifications of OTSs. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. Lecture Notes in Computer Science, vol.\u00a08373, pp. 630\u2013656. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_31","DOI":"10.1007\/978-3-642-54624-2_31"},{"key":"1_CR24","unstructured":"Pnueli, A.: Deduction is forever (1999), invited talk at FM\u201999 avaliable online at cs.nyu.edu\/pnueli\/fm99.ps"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Rocha, C., Meseguer, J.: Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool. In: Specification, Algebra, and Software\u2014Essays Dedicated to Kokichi Futatsugi. Lecture Notes in Computer Science, vol.\u00a08373, pp. 603\u2013629. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54624-2_30"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Rubio, R., Riesco, A.: Theorem proving for maude specifications using lean. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering\u201423rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13478, pp. 263\u2013280. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_16","DOI":"10.1007\/978-3-031-17244-1_16"},{"issue":"4","key":"1_CR27","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"JR Slagle","year":"1974","unstructured":"Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622\u2013642 (1974)","journal-title":"J. ACM"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Tran, D.D., Ogata, K.: IPSG: invariant proof score generator. In: Leong, H.V., Sarvestani, S.S., Teranishi, Y., Cuzzocrea, A., Kashiwazaki, H., Towey, D., Yang, J., Shahriar, H. (eds.) 46th IEEE Annual Computers, Software, and Applications Conferenc, COMPSAC 2022, Los Alamitos, CA, USA, June 27\u2013July 1, 2022. pp. 1050\u20131055. IEEE (2022). https:\/\/doi.org\/10.1109\/COMPSAC54236.2022.00164","DOI":"10.1109\/COMPSAC54236.2022.00164"}],"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_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:11:09Z","timestamp":1722496269000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}