{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:09Z","timestamp":1763468109763},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642327582"},{"type":"electronic","value":"9783642327599"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_32","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T10:12:30Z","timestamp":1345543950000},"page":"387-402","source":"Crossref","is-referenced-by-count":13,"title":["From Hoare Logic to Matching Logic Reachability"],"prefix":"10.1007","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"\u015etef\u0103nescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"issue":"1","key":"32_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science\u00a096(1), 217\u2013248 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"32_CR3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"32_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., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"issue":"1","key":"32_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing\u00a07(1), 70\u201390 (1978)","journal-title":"SIAM Journal on Computing"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Ellison, C.: Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544 (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"32_CR7","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT (2009)"},{"key":"32_CR8","unstructured":"George, C., Haxthausen, A.E., Hughes, S., Milne, R., Prehn, S., Pedersen, J.S.: The RAISE Development Method. BCS Practitioner Series. Prentice-Hall (1995)"},{"issue":"1-2","key":"32_CR9","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. The Journal of Logic and Algebraic Programming\u00a058(1-2), 61\u201388 (2004)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-540-30142-4_14","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Liu","year":"2004","unstructured":"Liu, H., Moore, J.S.: Java Program Verification via a JVM Deep Embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 184\u2013200. Springer, Heidelberg (2004)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"32_CR12","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 textbook. Formal Aspects of Computing\u00a010, 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"issue":"6","key":"32_CR13","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. The Journal of Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Matching logic: A new program verification approach (NIER track). In: ICSE, pp. 868\u2013871 (2011)","DOI":"10.1145\/1985793.1985928"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: From Hoare logic to matching logic reachability. Tech. Rep. Univ. of Illinois (June 2012), \n                  \n                    http:\/\/hdl.handle.net\/2142\/31335","DOI":"10.1007\/978-3-642-32759-9_32"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a07392, pp. 351\u2013363. Springer, Heidelberg (2012)"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"Algebraic Methodology and Software Technology","author":"G. Ro\u015fu","year":"2011","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: Matching Logic: An Alternative to Hoare\/Floyd Logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol.\u00a06486, pp. 142\u2013162. Springer, Heidelberg (2011)"},{"issue":"4","key":"32_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2007.06.006","volume":"176","author":"R. Sasse","year":"2007","unstructured":"Sasse, R., Meseguer, J.: Java+ITP: A verification tool based on Hoare logic and algebraic semantics. Electronic Notes in Theoretical Computer Science\u00a0176(4), 29\u201346 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:14:57Z","timestamp":1620130497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}