{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T14:40:07Z","timestamp":1746369607692,"version":"3.40.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319109350"},{"type":"electronic","value":"9783319109367"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10936-7_3","type":"book-chapter","created":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T15:17:55Z","timestamp":1410016675000},"page":"34-50","source":"Crossref","is-referenced-by-count":6,"title":["Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Bakhirkin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josh","family":"Berdine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11609773_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Arnold","year":"2006","unstructured":"Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining shape analyses by intersecting abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 33\u201348. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/s10009-007-0029-y","volume":"9","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT\u00a09(3-4), 413\u2013414 (2007)","journal-title":"STTT"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Berdine, J., Piterman, N.: Backward analysis via over-approximate abstraction and under-approximate subtraction. Tech. Rep. MSR-TR-2014-82, Microsoft Research (2014)","DOI":"10.1007\/978-3-319-10936-7_3"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-45221-5_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Berdine","year":"2013","unstructured":"Berdine, J., Bj\u00f8rner, N., Ishtiaq, S., Kriener, J.E., Wintersteiger, C.M.: Resourceful reachability as HORN-LA. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 137\u2013146. Springer, Heidelberg (2013)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"T.A. Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Ishtiaq, S.S., O\u2019Hearn, P.W.: Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In: PPDP, pp. 190\u2013201 (2000)","DOI":"10.1145\/351268.351291"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: APLAS, pp. 289\u2013300 (2001)","DOI":"10.1007\/3-540-45294-X_10"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M.: Program invariants as fixed points (preliminary reports). In: FOCS, pp. 18\u201329. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.25"},{"key":"3_CR10","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, pp. 303\u2013342. Prentice-Hall (1981)"},{"issue":"2&3","key":"3_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program.\u00a013(2&3), 103\u2013179 (1992)","journal-title":"J. Log. Program."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 147\u2013158. ACM (2008)","DOI":"10.1145\/1328897.1328459"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Method. Syst. Des.\u00a011(2), 157\u2013185 (1997)","journal-title":"Form. Method. Syst. Des."},{"key":"3_CR15","unstructured":"Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tech. Rep. TR-2007-12-01, Tel Aviv University (December 2007)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L. Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.entcs.2012.09.009","volume":"287","author":"A. Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Inferring sufficient conditions with backward polyhedral under-approximations. Electr. Notes Theor. Comput. Sci.\u00a0287, 89\u2013100 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1016\/j.scico.2012.07.004","volume":"78","author":"C. Popeea","year":"2013","unstructured":"Popeea, C., Chin, W.N.: Dual analysis for proving safety and finding bugs. Sci. Comput. Program.\u00a078(4), 390\u2013411 (2013)","journal-title":"Sci. Comput. Program."},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 380\u2013398. Springer, Heidelberg (2003)"},{"key":"3_CR20","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.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"3_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11924661_11","volume-title":"Programming Languages and Systems","author":"A. Simon","year":"2006","unstructured":"Simon, A., King, A.: Widening polyhedra with landmarks. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 166\u2013182. Springer, Heidelberg (2006)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79124-9_11","volume-title":"Tests and Proofs","author":"H. Velroyen","year":"2008","unstructured":"Velroyen, H., R\u00fcmmer, P.: Non-termination checking for imperative programs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 154\u2013170. Springer, Heidelberg (2008)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T.W., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Trans. Comput. Log. 8(1) (2007)","DOI":"10.1145\/1182613.1182618"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10936-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T14:18:17Z","timestamp":1746368297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10936-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319109350","9783319109367"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10936-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}