{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T10:11:13Z","timestamp":1781086273873,"version":"3.54.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319089171","type":"print"},{"value":"9783319089188","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_29","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:44:22Z","timestamp":1404279862000},"page":"425-440","source":"Crossref","is-referenced-by-count":39,"title":["All-Path Reachability Logic"],"prefix":"10.1007","author":[{"given":"Andrei","family":"\u015etef\u0103nescu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Mereuta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brandon M.","family":"Moore","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Traian Florin","family":"\u015eerb\u0103nut\u0103","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"Tobias 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":"1-2","key":"29_CR2","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. J. Logic and Algebraic Programming\u00a058(1-2), 61\u201388 (2004)","journal-title":"J. Logic and Algebraic Programming"},{"key":"29_CR3","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)"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Checking reachability using matching logic. In: OOPSLA, pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2398857.2384656"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-32759-9_32","volume-title":"FM 2012: Formal Methods","author":"G. Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: From hoare logic to matching logic reachability. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 387\u2013402. Springer, Heidelberg (2012)"},{"key":"29_CR6","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":"29_CR7","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, C., Moore, B.M.: One-path reachability logic. In: LICS 2013. IEEE (2013)","DOI":"10.1109\/LICS.2013.42"},{"key":"29_CR8","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":"6","key":"29_CR9","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"Grigore Ro\u0219u","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nut\u0103, T.F.: An overview of the K semantic framework. J. Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"29_CR11","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT (2009)"},{"issue":"1","key":"29_CR12","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":"1","key":"29_CR13","first-page":"47","volume":"18","author":"J. Matthews","year":"2008","unstructured":"Matthews, J., Findler, R.B.: An operational semantics for Scheme. JFP\u00a018(1), 47\u201386 (2008)","journal-title":"JFP"},{"key":"29_CR14","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, C., Moore, B.M., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: Reachability Logic in K. Technical Report. University of Illinois (November 2013), http:\/\/hdl.handle.net\/2142\/46296"},{"key":"29_CR15","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/978-3-662-44202-9_23","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"Daniele Filaretti","year":"2014","unstructured":"Filaretti, D., Maffeis, S.: An executable formal semantics of php. In: ECOOP. LNCS (to appear, 2014)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"10","key":"29_CR17","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. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"issue":"5","key":"29_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Communications of the ACM"},{"key":"29_CR19","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R.E.A. (ed.) Information Processing 1983: World Congress Proceedings, pp. 321\u2013332. Elsevier (1984)"},{"issue":"1-3","key":"29_CR20","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315\u2013327. ACM (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"issue":"1","key":"29_CR24","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/2103621.2103695","volume":"47","author":"Uday S. Reddy","year":"2012","unstructured":"Reddy, U.S., Reynolds, J.C.: Syntactic control of interference for separation logic. In: POPL, pp. 323\u2013336. ACM (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"29_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-23217-6_15","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"J. Hayman","year":"2011","unstructured":"Hayman, J.: Granularity and concurrent separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 219\u2013234. Springer, Heidelberg (2011)"},{"key":"29_CR26","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA, pp. 81\u201396 (2013)"},{"key":"29_CR27","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":"29_CR28","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.A.: Rewriting modulo smt and open system analysis. In: WRLA. LNCS (to appear, 2014)"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:44:46Z","timestamp":1746290686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}