{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:08:47Z","timestamp":1763467727661},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540330455"},{"type":"electronic","value":"9783540330462"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11690634_7","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:15:28Z","timestamp":1143555328000},"page":"94-110","source":"Crossref","is-referenced-by-count":33,"title":["A Logic of Reachable Patterns in Linked Data-Structures"],"prefix":"10.1007","author":[{"given":"Greta","family":"Yorsh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Rabinovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antoine","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/0196-6774(91)90006-K","volume":"12","author":"S. Arnborg","year":"1991","unstructured":"Arnborg, S., Lagergren, J., Seese, D.: Easy problems for tree-decomposable graphs. J. Algorithms\u00a012(2), 308\u2013340 (1991)","journal-title":"J. Algorithms"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: European Symp. On Programming, march 1999, pp. 2\u201319 (1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, Springer, Heidelberg (2004)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, Springer, Heidelberg (2005)"},{"key":"7_CR6","volume-title":"VISSAS intern. workshop","author":"M. Bozga","year":"2005","unstructured":"Bozga, M., Iosif, R.: Quantitative Verification of Programs with Lists. In: VISSAS intern. workshop, IOS Press, Amsterdam (2005)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Static Analysis Symp., pp. 344\u2013360 (2004)","DOI":"10.1007\/978-3-540-27864-1_25"},{"issue":"3","key":"7_CR8","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of jml tools and applications. Int. J. on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_25","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Calcagno","year":"2005","unstructured":"Calcagno, C., Gardner, P., Hague, M.: From Separation Logic to First-Order Logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, Springer, Heidelberg (2005)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, Springer, Heidelberg (2001)"},{"issue":"4","key":"7_CR11","first-page":"187","volume":"21","author":"B. Courcelle","year":"1989","unstructured":"Courcelle, B.: The monadic second-order logic of graphs, ii: Infinite graphs of bounded width. Mathematical Systems Theory\u00a021(4), 187\u2013221 (1989)","journal-title":"Mathematical Systems Theory"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0304-3975(01)00151-7","volume":"288","author":"E. Gr\u00e4del","year":"2002","unstructured":"Gr\u00e4del, E.: Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science\u00a0288, 129\u2013152 (2002)","journal-title":"Theoretical Computer Science"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s001530050130","volume":"38","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Archive of Math. Logic\u00a038, 313\u2013354 (1999)","journal-title":"Archive of Math. Logic"},{"key":"7_CR14","volume-title":"LICS 1999","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Walukiewicz, I.: Guarded Fixed Point Logic. In: LICS 1999, IEEE, Los Alamitos (1999)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Graedel, E., Kolaitis, P., Vardi, M.: On the decision problem for two variable logic. Bulletin of Symbolic Logic (1997)","DOI":"10.2307\/421196"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY (January 1990)","DOI":"10.1145\/318789.318812"},{"key":"7_CR17","first-page":"249","volume-title":"SIGPLAN Conf. on Prog. Lang. Design and Impl.","author":"L. Hendren","year":"1992","unstructured":"Hendren, L., Hummel, J., Nicolau, A.: Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., June 1992, pp. 249\u2013260. ACM Press, New York (1992)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, Springer, Heidelberg (1995)"},{"issue":"2","key":"7_CR19","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C.A.R. Hoare","year":"1975","unstructured":"Hoare, C.A.R.: Recursive data structures. Int. J. of Comp. and Inf. Sci.\u00a04(2), 105\u2013132 (1975)","journal-title":"Int. J. of Comp. and Inf. Sci."},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1137\/0216051","volume":"16","author":"N. Immerman","year":"1987","unstructured":"Immerman, N.: Languages that capture complexity classes. SIAM Journal of Computing\u00a016, 760\u2013778 (1987)","journal-title":"SIAM Journal of Computing"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundery between decidability and undecidability of transitive closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, Springer, Heidelberg (2004)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_22","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures. In: POPL, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"key":"7_CR24","volume-title":"POPL 1993","author":"N. Klarlund","year":"1993","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph Types. In: POPL 1993, ACM, New York (1993)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Generalized records and spatial conjunction in role logic. In: Static Analysis Symp., Verona, Italy, August 26\u201328 (2004)","DOI":"10.1007\/978-3-540-27864-1_26"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Symp. on Princ. of Prog. Lang. (to appear, 2006)","DOI":"10.1145\/1111037.1111048"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., pp. 221\u2013231 (2001)","DOI":"10.1145\/381694.378851"},{"key":"7_CR29","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1002\/malq.19750210118","volume":"21","author":"M. Mortimer","year":"1975","unstructured":"Mortimer, M.: On languages with two variables. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik\u00a021, 135\u2013140 (1975)","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"7_CR30","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141, 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-27813-9_2","volume-title":"Computer Aided Verification","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Wilhelm, R.: Static program analysis via 3-valued logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 15\u201330. Springer, Heidelberg (2004)"},{"key":"7_CR32","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002, IEEE, Los Alamitos (2002)"},{"issue":"1","key":"7_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (2002)","DOI":"10.1145\/514188.514190"},{"key":"7_CR35","unstructured":"Seese, D.: Interpretability and tree automata: A simple way to solve algorithmic problems on graphs closely related to trees. In: Tree Automata and Languages, pp. 83\u2013114 (1992)"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Sagiv, M., Rabinovich, A., Bouajjani, A., Meyer, A.: A logic of reachable patterns in linked data-structures. Technical report, Tel Aviv University (2005) Available at: www.cs.tau.ac.il\/~gretay","DOI":"10.1007\/11690634_7"},{"key":"7_CR37","unstructured":"Yorsh, G., Sagiv, M., Rabinovich, A., Bouajjani, A., Meyer, A.: Verification framework based on the logic of reachable patterns (in preparation, 2005)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11690634_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T21:49:14Z","timestamp":1683409754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11690634_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330455","9783540330462"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/11690634_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}