{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T13:40:09Z","timestamp":1748785209360,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319268491"},{"type":"electronic","value":"9783319268507"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-26850-7_22","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T09:14:46Z","timestamp":1455959686000},"page":"322-336","source":"Crossref","is-referenced-by-count":1,"title":["Antichains for the Verification of Recursive Programs"],"prefix":"10.1007","author":[{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,23]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321. IEEE (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"22_CR3","volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"JR B\u00fcchi","year":"1990","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Lane, S.M., Siefkes, D. (eds.) The Collected Works of J. Richard B\u00fcchi. Springer, New York (1990)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62\u201373. ACM (2003)","DOI":"10.1145\/640128.604137"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-37064-9_18","volume-title":"Language and Automata Theory and Applications","author":"V Bruy\u00e8re","year":"2013","unstructured":"Bruy\u00e8re, V., Ducobu, M., Gauwin, O.: Visibly pushdown automata: universality and inclusion via antichains. In: Dediu, A.-H., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 190\u2013201. Springer, Heidelberg (2013)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: Artificial Intelligence and Programming Languages, pp. 1\u201312. ACM (1977)","DOI":"10.1145\/872736.806926"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/11730637_14","volume-title":"Hybrid Systems: Computation and Control","author":"M Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Raskin, J.-F.: A lattice theory for solving games of imperfect information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153\u2013168. Springer, Heidelberg (2006)"},{"issue":"6","key":"22_CR8","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. JACM 57(6), 33:1\u201333:47 (2010)","journal-title":"JACM"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL, pp. 129\u2013142. ACM (2013)","DOI":"10.1145\/2480359.2429086"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: POPL, pp. 151\u2013164. ACM (2014)","DOI":"10.1145\/2535838.2535885"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In: POPL, pp. 407\u2013420. ACM (2015)","DOI":"10.1145\/2775051.2677012"},{"issue":"1\u20132","key":"22_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-12002-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Fogarty","year":"2010","unstructured":"Fogarty, S., Vardi, M.Y.: Efficient B\u00fcchi universality checking. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 205\u2013220. Springer, Heidelberg (2010)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-642-39212-2_22","volume-title":"Automata, Languages, and Programming","author":"O Friedmann","year":"2013","unstructured":"Friedmann, O., Klaedtke, F., Lange, M.: Ramsey goes visibly pushdown. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 224\u2013237. Springer, Heidelberg (2013)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL, pp. 471\u2013482. ACM (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013)"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-78800-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lal","year":"2008","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282\u2013298. Springer, Heidelberg (2008)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-28872-2_25","volume-title":"Fundamental Approaches to Software Engineering","author":"Z Long","year":"2012","unstructured":"Long, Z., Calin, G., Majumdar, R., Meyer, R.: Language-theoretic abstraction refinement. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 362\u2013376. Springer, Heidelberg (2012)"},{"key":"22_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"issue":"2","key":"22_CR21","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49\u201361. ACM (1995)","DOI":"10.1145\/199448.199462"},{"key":"22_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17548-0","volume-title":"Compiler Design - Analysis and Transformation","author":"H Seidl","year":"2012","unstructured":"Seidl, H., Wilhelm, R., Hack, S.: Compiler Design - Analysis and Transformation. Springer, Heidelberg (2012)"},{"key":"22_CR24","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report 2, New York University (1978)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26850-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T13:04:50Z","timestamp":1748783090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26850-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319268491","9783319268507"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26850-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}