{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:28:11Z","timestamp":1774837691383,"version":"3.50.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,5,7]],"date-time":"2015-05-07T00:00:00Z","timestamp":1430956800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s00236-015-0235-0","type":"journal-article","created":{"date-parts":[[2015,5,6]],"date-time":"2015-05-06T11:29:56Z","timestamp":1430911796000},"page":"357-385","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verification of heap manipulating programs with ordered data by extended forest automata"],"prefix":"10.1007","volume":"53","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","published-online":{"date-parts":[[2015,5,7]]},"reference":[{"key":"235_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atto, M., Cederberg, J., Ji, R.: Automated analysis of data-dependent programs with dynamic memory. In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis\u2013ATVA\u201909, volume 5799 of LNCS, pp. 197\u2013212. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04761-9_16"},{"key":"235_CR2","doi-asserted-by":"crossref","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 Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u2013TACAS\u201913, volume 7795 of LNCS, pp. 324\u2013338. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"235_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P., 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. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis\u2013ATVA\u201913, volume 8172 of LNCS, pp. 224\u2013239. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_17"},{"key":"235_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In Proceedings of the 18th International Conference on Computer Aided Verification\u2013CAV\u201906, volume 4144 of LNCS, pp. 532\u2013546. Springer (2006)","DOI":"10.1007\/11817963_48"},{"key":"235_CR5","doi-asserted-by":"crossref","unstructured":"Bingham, J., Rakamari\u0107, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation\u2013VMCAI\u201906, volume 3855 of LNCS, pp. 207\u2013221. Springer (2006)","DOI":"10.1007\/11609773_14"},{"issue":"2","key":"235_CR6","doi-asserted-by":"crossref","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. Form. Methods Syst. Des. 38(2), 158\u2013192 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"235_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis\u2013ATVA\u201912, volume 7561 of LNCS, pp 167\u2013182. Springer (2012)","DOI":"10.1007\/978-3-642-33386-6_14"},{"issue":"2","key":"235_CR8","doi-asserted-by":"crossref","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. J. Softw. Tools Technol. Transf. 14(2), 167\u2013191 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"235_CR9","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y. E., Rival, X.: Relational inductive shape analysis. In Proceedings of the 35th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL\u201908, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"235_CR10","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In Proceedings of the 14th International Static Analysis Symposium\u2013SAS\u201907, volume 4634 of LNCS, pp. 384\u2013401. Springer (2007)","DOI":"10.1007\/978-3-540-74061-2_24"},{"key":"235_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, S., Lahiri, S. K., Qadeer, S., Rakaramari\u0107, Z.: A reachability predicate for analyzing low-level software. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u2013TACAS\u201907, volume 4424 of LNCS, pp. 19\u201333. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_4"},{"issue":"9","key":"235_CR12","doi-asserted-by":"crossref","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.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"235_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL\u201977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"235_CR14","doi-asserted-by":"crossref","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In Proceedings of the 20th International Static Analysis Symposium\u2013SAS\u201913, volume 7935 of LNCS, pp. 215\u2013237. Springer (2013)","DOI":"10.1007\/978-3-642-38856-9_13"},{"issue":"1","key":"235_CR15","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s10703-012-0150-8","volume":"41","author":"P Habermehl","year":"2012","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Form. Methods Syst. Des. 41(1), 83\u2013106 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"235_CR16","doi-asserted-by":"crossref","unstructured":"Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph grammar abstraction for unbounded heap structures. In Proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software\u2013TTSS\u201909, volume 266 of ENTCS, pp. 93\u2013107. Elsevier (2010)","DOI":"10.1016\/j.entcs.2011.07.001"},{"key":"235_CR17","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In Proceedings of the 25th International Conference on Computer Aided Verification\u2013CAV\u201913, volume 8044 of LNCS, pp. 740\u2013755. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_52"},{"key":"235_CR18","doi-asserted-by":"crossref","unstructured":"Jensen, J.L., J\u00f8rgensen, M. E., Schwartzbach, M. I., Klarlund, N.: Automatic verification of pointer programs using monadic second-order logic. In Proceedings of the 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation\u2013PLDI\u201997, pp. 226\u2013234. ACM (1997)","DOI":"10.1145\/258915.258936"},{"key":"235_CR19","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In Proceedings of the 35th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL\u201908, pp. 171\u2013182. ACM (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"235_CR20","doi-asserted-by":"crossref","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In Proceedings of the 17th International Conference on Computer Aided Verification\u2013CAV\u201905, volume 3576 of LNCS, pp. 519\u2013533. Springer (2005)","DOI":"10.1007\/11513988_50"},{"key":"235_CR21","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In Proceedings of the 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL\u201910, pp. 211\u2013222. ACM (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"235_CR22","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In Proceedings of the 17th International Conference on Computer Aided Verification\u2013CAV\u201905, volume 3576 of LNCS, pp. 476\u2013490. Springer (2005)","DOI":"10.1007\/11513988_47"},{"issue":"6","key":"235_CR23","doi-asserted-by":"crossref","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: a probabilistic alternative to balanced trees. Commun ACM 33(6), 668\u2013676 (1990)","journal-title":"Commun ACM"},{"key":"235_CR24","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1016\/j.jsc.2012.08.007","volume":"50","author":"S Qin","year":"2013","unstructured":"Qin, S., He, G., Luo, C., Chin, W.-N., Chen, X.: Loop invariant synthesis in a combined abstract domain. J. Symb. Comput. 50, 386\u2013408 (2013)","journal-title":"J. Symb. Comput."},{"key":"235_CR25","doi-asserted-by":"crossref","unstructured":"Rakamari\u0107, Z., Bruttomesso, R., Hu, A.J., Cimatti, A.: Verifying heap-manipulating programs in an SMT framework. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis\u2013ATVA\u201907, volume 4762 of LNCS, pp. 237\u2013252. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_18"},{"issue":"3","key":"235_CR26","doi-asserted-by":"crossref","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 Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"235_CR27","unstructured":"Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: On verifying complex properties using symbolic shape analysis. In Proceedings of Heap Analysis and Verification 2007\u2013HAV\u201907 (2007)"},{"key":"235_CR28","doi-asserted-by":"crossref","unstructured":"Wies, T., Podelski, A.: Counterexample-guided focus. In Proceedings of the 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL\u201910, pp. 249\u2013260. ACM (2010)","DOI":"10.1145\/1706299.1706330"},{"key":"235_CR29","doi-asserted-by":"crossref","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In Proceedings of the 20th International Conference on Computer Aided Verification\u2013CAV\u201908, volume 5123 of LNCS, pp. 385\u2013398. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"235_CR30","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation\u2013PLDI\u201908, pp. 349\u2013361. ACM (2008)","DOI":"10.1145\/1375581.1375624"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0235-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0235-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0235-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,24]],"date-time":"2019-08-24T17:08:22Z","timestamp":1566666502000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0235-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,7]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["235"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0235-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,7]]}}}