{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T13:02:52Z","timestamp":1746709372086},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642546235"},{"type":"electronic","value":"9783642546242"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54624-2_30","type":"book-chapter","created":{"date-parts":[[2014,2,28]],"date-time":"2014-02-28T17:42:59Z","timestamp":1393609379000},"page":"603-629","source":"Crossref","is-referenced-by-count":5,"title":["Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Eindhoven, The Netherlands, June 24-26. LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"issue":"5","key":"30_CR2","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K.A. Bartlett","year":"1969","unstructured":"Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commununications of the ACM\u00a012(5), 260\u2013261 (1969)","journal-title":"Commununications of the ACM"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/3-540-16444-8_1","volume-title":"Mathematical Methods of Specification and Synthesis of Software Systems 1985","author":"J. Bergstra","year":"1986","unstructured":"Bergstra, J., Klop, J.: Verification of an Alternating Bit Protocol by means of process algebra protocol. In: Bibel, W., Jantke, K. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems 1985. LNCS, vol.\u00a0215, pp. 9\u201323. Springer, Heidelberg (1986)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-48654-1_30","volume-title":"CONCUR \u201994: Concurrency Theory","author":"M. Bezem","year":"1994","unstructured":"Bezem, M., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 401\u2013416. Springer, Heidelberg (1994)"},{"issue":"1-3","key":"30_CR5","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. Theoretical Computer Science\u00a0360(1-3), 386\u2013414 (2006)","journal-title":"Theoretical Computer Science"},{"key":"30_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/11784180_28","volume-title":"Algebraic Methodology and Software Technology","author":"M. Clavel","year":"2006","unstructured":"Clavel, M., Egea, M.: ITP\/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 368\u2013373. Springer, Heidelberg (2006)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010)"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.tcs.2012.07.041","volume":"464","author":"K. Futatsugi","year":"2012","unstructured":"Futatsugi, K., G\u00e2in\u00e2, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoretical Computer Science\u00a0464, 90\u2013112 (2012)","journal-title":"Theoretical Computer Science"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-40206-7_26","volume-title":"CALCO 2013","author":"D. G\u0103in\u0103","year":"2013","unstructured":"G\u0103in\u0103, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol.\u00a08089, pp. 328\u2013333. Springer, Heidelberg (2013)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-61780-9_67","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1996","unstructured":"Gim\u00e9nez, E.: An application of co-inductive types in Coq: Verification of the Alternating Bit Protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 135\u2013152. Springer, Heidelberg (1996)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-34005-5_9","volume-title":"Rewriting Logic and Its Applications","author":"R. Guti\u00e9rrez","year":"2012","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 162\u2013181. Springer, Heidelberg (2012)"},{"key":"30_CR13","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)"},{"key":"30_CR14","unstructured":"Lin, K., Goguen, J.: A hidden proof of the Alternating Bit Protocol, \n                  \n                    http:\/\/cseweb.ucsd.edu\/~goguen\/pps\/abp.ps"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"issue":"7-8","key":"30_CR16","first-page":"721","volume":"81","author":"J. Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. JLAP\u00a081(7-8), 721\u2013781 (2012)","journal-title":"JLAP"},{"key":"30_CR17","unstructured":"Meseguer, J., Goguen, J.A.: Initially, induction and computability. Algebraic Methods in Semantics (1986)"},{"issue":"6","key":"30_CR18","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1142\/S0218194007003458","volume":"17","author":"M. Nakano","year":"2007","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Cr\u00e8me: an automatic invariant prover of behavioral specifications. International Journal of Software Engineering and Knowledge Engineering\u00a017(6), 783\u2013804 (2007)","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ Method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"30_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2008.02.018","volume":"201","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS\/CafeOBJ method. Electronic Notes in Theorethical Computer Science\u00a0201, 127\u2013154 (2008)","journal-title":"Electronic Notes in Theorethical Computer Science"},{"issue":"2","key":"30_CR21","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1142\/S0218194010004712","volume":"20","author":"K. Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. International Journal of Software Engineering and Knowledge Engineering\u00a020(2), 253\u2013287 (2010)","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"30_CR22","unstructured":"Pnueli, A.: Deduction is forever (1999) Invited talk at FM 1999 avaliable online at \n                  \n                    cs.nyu.edu\/pnueli\/fm99.ps"},{"key":"30_CR23","unstructured":"Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign (2012), \n                  \n                    http:\/\/hdl.handle.net\/2142\/42200"},{"key":"30_CR24","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.\u00a06859, pp. 314\u2013328. Springer, Heidelberg (2011)"},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Matching Logic: A New Program Verification Approach (NIER Track). In: ICSE 211: Proceedings of the 30th International Conference on Software Engineering, pp. 868\u2013871. ACM (2011)","DOI":"10.1145\/1985793.1985928"},{"key":"30_CR26","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S1571-0661(05)82554-X","volume":"15","author":"L. Steggles","year":"1998","unstructured":"Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: A case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science\u00a015, 83\u2013104 (1998)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"11","key":"30_CR27","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1109\/32.60315","volume":"16","author":"I. Suzuki","year":"1990","unstructured":"Suzuki, I.: Formal analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering\u00a016(11), 1273\u20131281 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"30_CR28","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. TCS\u00a0285, 487\u2013517 (2002)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Specification, Algebra, and Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54624-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T06:06:46Z","timestamp":1558850806000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54624-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642546235","9783642546242"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54624-2_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}