{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:35Z","timestamp":1777890995541,"version":"3.51.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_16","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"288-309","source":"Crossref","is-referenced-by-count":6,"title":["Counterexample Validation and Interpolation-Based Refinement for Forest Automata"],"prefix":"10.1007","author":[{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hru\u0161ka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","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":[[2017,1,12]]},"reference":[{"issue":"4","key":"16_CR1","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s00236-015-0235-0","volume":"53","author":"PA Abdulla","year":"2016","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. Acta Informatica 53(4), 357\u2013385 (2016). http:\/\/dx.doi.org\/ 10.1007\/s00236-015-0235-0","journal-title":"Acta Informatica"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-662-46669-8_26","volume-title":"Programming Languages and Systems","author":"A Albargouthi","year":"2015","unstructured":"Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634\u2013660. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46669-8_26"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31424-7_16","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2012","unstructured":"Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing abstraction failure for separation logic\u2013based analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 155\u2013173. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_16"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 532\u2013546. Springer, Heidelberg (2006). doi: 10.1007\/11817963_48"},{"key":"16_CR5","unstructured":"Botin\u010dan, M., Dodds, M., Magill, S.: Refining existential properties in separation logic analyses. Technical report (2015). arXiv:1504.08309"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","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. 3440, pp. 13\u201329. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31980-1_2"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11823230_5","volume-title":"Static Analysis","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 52\u201370. Springer, Heidelberg (2006). doi: 10.1007\/11823230_5"},{"issue":"2","key":"16_CR8","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":"16_CR9","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. 7561, pp. 167\u2013182. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33386-6_14"},{"issue":"2","key":"16_CR10","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":"16_CR11","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-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74061-2_24"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11691372_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JV Deshmukh","year":"2006","unstructured":"Deshmukh, J.V., Emerson, E.A., Gupta, P.: Automatic verification of parameterized data structures. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 27\u201341. Springer, Heidelberg (2006). doi: 10.1007\/11691372_2"},{"key":"16_CR13","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.) SAS 2013. LNCS, vol. 7935, pp. 215\u2013237. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38856-9_13"},{"issue":"1","key":"16_CR14","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":"16_CR15","doi-asserted-by":"crossref","unstructured":"Heinen, J., Noll, T., Rieger, S.: Juggrnaut: graph grammar abstraction for unbounded heap structures. In: Proceedings of 3rd International Workshop on Harnessing Theories for Tool Support in Software\u2013TTSS 2009. ENTCS, vol. 266, pp. 93\u2013107. Elsevier (2010)","DOI":"10.1016\/j.entcs.2011.07.001"},{"key":"16_CR16","unstructured":"Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., Rogalewicz, A., Vojnar, T.: Counterexample validation and interpolation-based refinement for forest automata. Technical report FIT-TR-2016-03 (2016). http:\/\/www.fit.vutbr.cz\/~lengal\/pub\/FIT-TR-2016-03.pdf"},{"key":"16_CR17","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. 8044, pp. 740\u2013755. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_52"},{"key":"16_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 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation\u2013PLDI 1997, pp. 226\u2013234. ACM (1997)","DOI":"10.1145\/258915.258936"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). doi: 10.1007\/11817963_14"},{"key":"16_CR20","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. 3576, pp. 519\u2013533. Springer, Heidelberg (2005). doi: 10.1007\/11513988_50"},{"key":"16_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 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL 2010, pp. 211\u2013222. ACM (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_1"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: Proceedings of 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages\u2013POPL 2010, pp. 249\u2013260. ACM (2010)","DOI":"10.1145\/1706299.1706330"},{"key":"16_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. Symbol. Comput. 50, 386\u2013408 (2013)","journal-title":"J. Symbol. Comput."},{"issue":"3","key":"16_CR25","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":"16_CR26","unstructured":"\u0160im\u00e1\u010dek, J.: Harnessing forest automata for verification of heap manipulating programs. Ph.D. thesis, Grenoble Alpes University, France (2012). https:\/\/tel.archives-ouvertes.fr\/tel-00805794"},{"key":"16_CR27","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. 5123, pp. 385\u2013398. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_36"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T03:53:55Z","timestamp":1498362835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}