{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:06:56Z","timestamp":1748664416481,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662482872"},{"type":"electronic","value":"9783662482889"}],"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-662-48288-9_8","type":"book-chapter","created":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T02:26:24Z","timestamp":1441074384000},"page":"128-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR"],"prefix":"10.1007","author":[{"given":"Tachio","family":"Terauchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,2]]},"reference":[{"key":"8_CR1","unstructured":"International competition on software verification (SV-COMP). http:\/\/sv-comp.sosy-lab.org\/"},{"key":"8_CR2","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Longman Publishing Co., Inc., Boston (1986)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina and Veith [18], pp. 313\u2013329","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) POPL, pp. 1\u20133. ACM (2002)","DOI":"10.1145\/503272.503274"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) STOC, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"8_CR7","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: Graham, R.M., Harrison, M.A., Sethi, R. (eds.), POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1\u20134","key":"8_CR8","first-page":"27","volume":"5","author":"J Esparza","year":"2008","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. JSAT 5(1\u20134), 27\u201356 (2008)","journal-title":"JSAT"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Symposia in Applied Mathematics, vol.19, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"16","key":"8_CR10","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2010.05.021","volume":"110","author":"BS Gulavani","year":"2010","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Refining abstract interpretations. Inf. Process. Lett. 110(16), 666\u2013671 (2010)","journal-title":"Inf. Process. Lett."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the grey area of proofs. In: Field, J., Hicks, M. (eds.) POPL, pp. 259\u2013272. ACM (2012)","DOI":"10.1145\/2103621.2103689"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"8_CR14","unstructured":"N. Kobayashi. Personal communication, 30 Aug (2012)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Sharygina and Veith [18], pp. 347\u2013363","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Scholl, C., Pigorsch, F., Disch, S., Althaus, E.: Simple interpolants for linear arithmetic. In: DATE, pp. 1\u20136. IEEE (2014)","DOI":"10.7873\/DATE2014.128"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2013","unstructured":"Sharygina, N., Veith, H. (eds.): CAV 2013. LNCS, vol. 8044. Springer, Heidelberg (2013)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1707801.1706315"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Explaining the effectiveness of small refinement heuristics in program verification with CEGAR (2015). http:\/\/www.jaist.ac.jp\/terauchi","DOI":"10.1007\/978-3-662-48288-9_8"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/978-3-662-46669-8_25","volume-title":"Programming Languages and Systems","author":"T Terauchi","year":"2015","unstructured":"Terauchi, T., Unno, H.: Relaxed stratification: a new approach to practical complete predicate refinement. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 610\u2013633. Springer, Heidelberg (2015)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-662-46681-0_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Unno","year":"2015","unstructured":"Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free horn clauses via sampling. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 149\u2013163. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48288-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T09:57:57Z","timestamp":1748599077000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-48288-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662482872","9783662482889"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48288-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"2 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}