{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:46:37Z","timestamp":1760013997970},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_17","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T01:11:21Z","timestamp":1377738681000},"page":"224-239","source":"Crossref","is-referenced-by-count":11,"title":["Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong Quy","family":"Trinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-04761-9_16","volume-title":"Automated Technology for Verification and Analysis","author":"P.A. Abdulla","year":"2009","unstructured":"Abdulla, P.A., Atto, M., Cederberg, J., Ji, R.: Automated Analysis of Data-Dependent Programs with Dynamic Memory. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 197\u2013212. Springer, Heidelberg (2009)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 324\u2013338. Springer, Heidelberg (2013)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-02444-8_17","volume-title":"Automated Technology for Verification and Analysis","author":"Parosh Aziz Abdulla","year":"2013","unstructured":"Abdulla, P.A., Hol\u00edk, L., Jonsson, B., Leng\u00e1l, O., Trinh, C.Q., Vojnar, T.: Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Technical report FIT-TR-2013-02, FIT BUT (2013)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Bingham","year":"2006","unstructured":"Bingham, J., Rakamari\u0107, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 207\u2013221. Springer, Heidelberg (2006)"},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10703-011-0111-7","volume":"38","author":"A. Bouajjani","year":"2011","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists Are Counter Automata. Formal Methods in System Design\u00a038(2), 158\u2013192 (2011)","journal-title":"Formal Methods in System Design"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-33386-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 167\u2013182. Springer, Heidelberg (2012)"},{"issue":"2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-011-0205-y","volume":"14","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular (Tree) Model Checking. Int. Journal on Software Tools for Technology Transfer\u00a014(2), 167\u2013191 (2012)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B.-Y.E. Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape Analysis with Structural Invariant Checkers. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 384\u2013401. Springer, Heidelberg (2007)"},{"issue":"9","key":"17_CR9","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W.-N. Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H., Qin, S.: Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic. Science of Computer Programming\u00a077(9), 1006\u20131036 (2012)","journal-title":"Science of Computer Programming"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38856-9_13","volume-title":"Static Analysis","author":"K. Dudka","year":"2013","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-Precise Verification of Low-Level List Manipulation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol.\u00a07935, pp. 215\u2013237. Springer, Heidelberg (2013)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-22110-1_34","volume-title":"Computer Aided Verification","author":"P. Habermehl","year":"2011","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 424\u2013440. Springer, Heidelberg (2011)"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2011.07.001","volume":"266","author":"Jonathan Heinen","year":"2010","unstructured":"Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. ENTCS, vol. 266 (2010)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/978-3-642-39799-8_52","volume-title":"Computer Aided Verification","author":"L. Hol\u00edk","year":"2013","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully Automated Shape Analysis Based on Forest Automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 740\u2013755. Springer, Heidelberg (2013), \n                    \n                      http:\/\/arxiv.org\/abs\/1304.5806"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Jensen, J., J\u00f8rgensen, M., Klarlund, N., Schwartzbach, M.: Automatic Verification of Pointer Programs Using Monadic Second-order Logic. In: Proc. of PLDI 1997. ACM (1997)","DOI":"10.1145\/258915.258936"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"17_CR16","unstructured":"Magill, S., Tsai, M., Lee, P., Tsay, Y.-K.: A Calculus of Atomic Actions. In: POPL 2010. ACM (2010)"},{"issue":"6","key":"17_CR17","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"William Pugh","year":"1990","unstructured":"Pugh, W.: Skip Lists: A Probabilistic Alternative to Balanced Trees. CACM\u00a033(6) (1990)","journal-title":"Communications of the ACM"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.jsc.2012.08.007","volume":"50","author":"Shengchao Qin","year":"2013","unstructured":"Qin, S., He, G., Luo, C., Chin, W.-N., Chen, X.: Loop Invariant Synthesis in a Combined Abstract Domain. Journal of Symbolic Computation\u00a050 (2013)","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"17_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"Mooly Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T., Wilhelm, R.: Parametric Shape Analysis via 3-valued Logic. TOPLAS\u00a024(3) (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR20","unstructured":"Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: On Verifying Complex Properties using Symbolic Shape Analysis. In: Proc. of HAV 2007 (2007)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"},{"issue":"6","key":"17_CR22","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1379022.1375624","volume":"43","author":"Karen Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full Functional Verification of Linked Data Structures. In: Proc. of PLDI 2008. ACM Press (2008)","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T20:23:54Z","timestamp":1558038234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}