{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T06:22:01Z","timestamp":1770963721520,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319155784","type":"print"},{"value":"9783319155791","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15579-1_2","type":"book-chapter","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T08:36:13Z","timestamp":1424680573000},"page":"25-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated Program Verification"],"prefix":"10.1007","author":[{"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,24]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3) (2009)","DOI":"10.1145\/1516512.1516518"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-36742-7_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Christ","year":"2013","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 124\u2013138. Springer, Heidelberg (2013)"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic 10(3), 16:1\u201316:30 (2009)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR4","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":"2_CR5","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: POPL, pp. 151\u2013164. ACM (2014)","DOI":"10.1145\/2578855.2535885"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In: POPL. ACM (2015)","DOI":"10.1145\/2676726.2677012"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Figueira, D.: Alternating register automata on finite words and trees. Logical Methods in Computer Science 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:22)2012"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-54862-8_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., et al.: Ultimate automizer with unsatisfiable cores (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 418\u2013420. Springer, Heidelberg (2014)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Heidelberg (2013)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009)"},{"key":"2_CR11","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":"2_CR12","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":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797\u2013813. Springer, Heidelberg (2014)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-34281-3_23","volume-title":"Formal Methods and Software Engineering","author":"M Junker","year":"2012","unstructured":"Junker, M., Huuck, R., Fehnker, A., Knapp, A.: SMT-based false positive elimination in static program analysis. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 316\u2013331. Springer, Heidelberg (2012)"},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-54862-8_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Leike","year":"2014","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014)"},{"issue":"3","key":"2_CR17","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR18","series-title":"lecture notes in computer science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49\u201361. ACM (1995)","DOI":"10.1145\/199448.199462"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Sch\u00e4f, M., Schwartz-Narbonne, D., Wies, T.: Explaining inconsistent code. In: ESEC\/FSE, pp. 521\u2013531. ACM (2013)","DOI":"10.1145\/2491411.2491448"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15579-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T02:25:48Z","timestamp":1675131948000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15579-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155784","9783319155791"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15579-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"24 February 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}