{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:02Z","timestamp":1747592462269},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"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_17","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"310-329","source":"Crossref","is-referenced-by-count":4,"title":["Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT"],"prefix":"10.1007","author":[{"given":"Jiahong","family":"Jiang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liqian","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xueguang","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"17_CR1","unstructured":"http:\/\/sv-comp.sosy-lab.org\/2015\/"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-28756-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 157\u2013172. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_12"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_48"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Static Analysis","author":"X Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, \u00c9.: Inferring min and max invariants using max-plus polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 189\u2013204. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69166-2_13"},{"key":"17_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 2009, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"17_CR6","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD 2010, pp. 189\u2013198. IEEE (2010)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$\\nu Z$$ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_14"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-662-48288-9_3","volume-title":"Static Analysis","author":"J Chen","year":"2015","unstructured":"Chen, J., Cousot, P.: A binary decision tree abstract domain functor. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 36\u201353. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48288-9_3"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-319-10936-7_7","volume-title":"Static Analysis","author":"L Chen","year":"2014","unstructured":"Chen, L., Liu, J., Min\u00e9, A., Kapur, D., Wang, J.: An abstract domain to infer octagonal constraints with absolute value. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 101\u2013117. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-10936-7_7"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-03237-0_21","volume-title":"Static Analysis","author":"L Chen","year":"2009","unstructured":"Chen, L., Min\u00e9, A., Wang, J., Cousot, P.: Interval polyhedra: an abstract domain to infer interval linear relationships. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 309\u2013325. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03237-0_21"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-19718-5_9","volume-title":"Programming Languages and Systems","author":"L Chen","year":"2011","unstructured":"Chen, L., Min\u00e9, A., Wang, J., Cousot, P.: Linear absolute value relation analysis. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 156\u2013175. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19718-5_9"},{"key":"17_CR12","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: POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"17_CR13","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does astr\u00e9e scale up? Formal Methods Syst. Des. 35(3), 229\u2013264 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-19805-2_31","volume-title":"Foundations of Software Science and Computational Structures","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 456\u2013472. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19805-2_31"},{"issue":"4","key":"17_CR15","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: ESEC-FSE 2005, pp. 227\u2013236. ACM (2005)","DOI":"10.1145\/1081706.1081742"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-27940-9_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K Ghorbal","year":"2012","unstructured":"Ghorbal, K., Ivan\u010di\u0107, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 235\u2013250. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-27940-9_16"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-15769-1_18","volume-title":"Static Analysis","author":"A Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287\u2013303. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15769-1_18"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-20398-5_11","volume-title":"NASA Formal Methods","author":"A Gurfinkel","year":"2011","unstructured":"Gurfinkel, A., Chaki, S., Sapra, S.: Efficient predicate abstraction of program summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 131\u2013145. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_11"},{"key":"17_CR20","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-642-33125-1_20","volume-title":"Static Analysis","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: Succinct representations for abstract interpretation. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 283\u2013299. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33125-1_20"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-662-53413-7_12","volume-title":"Static Analysis","author":"K Heo","year":"2016","unstructured":"Heo, K., Oh, H., Yang, H.: Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 237\u2013256. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53413-7_12"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_52"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, vol. 49, pp. 607\u2013618. ACM (2014)","DOI":"10.1145\/2535838.2535857"},{"issue":"1","key":"17_CR25","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"issue":"3","key":"17_CR26","doi-asserted-by":"crossref","first-page":"501","DOI":"10.2168\/LMCS-6(3:4)2010","volume":"6","author":"D Monniaux","year":"2010","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints. Log. Methods Comput. Sci. 6(3), 501\u2013516 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-23702-7_27","volume-title":"Static Analysis","author":"D Monniaux","year":"2011","unstructured":"Monniaux, D., Gonnord, L.: Using bounded model checking to focus fixpoint iterations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 369\u2013385. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_27"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Monniaux, D.P.: Automatic modular abstractions for linear constraints. In: POPL 2009, vol. 44, pp. 140\u2013151. ACM (2009)","DOI":"10.1145\/1594834.1480899"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45937-5_16"},{"issue":"3","key":"17_CR30","first-page":"1","volume":"36","author":"O Hakjoo","year":"2014","unstructured":"Hakjoo, O., Heo, K., Lee, W., Lee, W., Park, D., Kang, J., Yi, K.: Global sparse analysis framework. ACM Trans. Program. Lang. Syst. 36(3), 1\u201344 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24622-0_21"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25\u201341. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-30579-8_2"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-33125-1_10","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 111\u2013128. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33125-1_10"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174\u2013192. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_17"}],"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_17","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_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}