{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:44Z","timestamp":1763468024618,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642177958"},{"type":"electronic","value":"9783642177965"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-17796-5_9","type":"book-chapter","created":{"date-parts":[[2011,1,11]],"date-time":"2011-01-11T17:08:27Z","timestamp":1294765707000},"page":"142-162","source":"Crossref","is-referenced-by-count":25,"title":["Matching Logic: An Alternative to Hoare\/Floyd Logic"],"prefix":"10.1007","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[]},{"given":"Chucky","family":"Ellison","sequence":"additional","affiliation":[]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"9_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"9_CR5","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Tech. Rep. MSR-TR-2009-15, Microsoft Research (2009)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. In: OOPSLA 2008, pp. 213\u2013226 (2008)","DOI":"10.1145\/1449955.1449782"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"9_CR10","first-page":"19","volume-title":"Proceedings of the Symposium on Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, 19th edn., pp. 19\u201332. AMS, Providence (1967)","edition":"19"},{"key":"9_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"J. Goguen","year":"1996","unstructured":"Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)"},{"key":"9_CR12","series-title":"History of Computing Series","volume-title":"Reflections on the Work of C.A.R.\u00a0Hoare","author":"M. Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Reflections on the Work of C.A.R.\u00a0Hoare. History of Computing Series, Springer, Heidelberg (2010)"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00289068","volume":"11","author":"D. Gries","year":"1979","unstructured":"Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informatica\u00a011, 223\u2013232 (1979)","journal-title":"Acta Informatica"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Handbook of Philosophical Logic, pp. 497\u2013604 (1984)","DOI":"10.1007\/978-94-009-6259-0_10"},{"issue":"10","key":"9_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM\u00a012(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Hubert, T., March\u00e9, C.: A case study of C source code verification: The Schorr-Waite algorithm. In: SEFM 2005, pp. 190\u2013199 (2005)","DOI":"10.1109\/SEFM.2005.1"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006, pp. 115\u2013126 (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"9_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S.: Simulating reachability using first-order logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11823230_17","volume-title":"Static Analysis","author":"A. Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 261\u2013279. Springer, Heidelberg (2006)"},{"issue":"3","key":"9_CR20","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. Theoretical Computer Science\u00a0373(3), 213\u2013237 (2007)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"9_CR21","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/381694.378851","volume":"36","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. SIGPLAN Not.\u00a036(5), 221\u2013231 (2001)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"9_CR22","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics. Formal Aspects of Computing\u00a010(2), 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05, 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: ASE 2001, pp. 157\u2013165 (2001)","DOI":"10.1109\/ASE.2001.989801"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9_CR26","unstructured":"Ro\u015fu, G., Schulte, W.: Matching logic\u2013Extended report. Tech. Rep. UIUCDCS-R-2009-3026, University of Illinois (2009)"},{"key":"9_CR27","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: From rewriting logic executable semantics to matching logic program verification. Tech. Rep. UIUC (2009), http:\/\/hdl.handle.net\/2142\/13159"},{"issue":"6","key":"9_CR28","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. Journal of Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"3","key":"9_CR29","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17796-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T16:20:29Z","timestamp":1740846029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17796-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642177958","9783642177965"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17796-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}