{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:06:15Z","timestamp":1725768375356},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_17","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"302-321","source":"Crossref","is-referenced-by-count":11,"title":["Generic Combination of Heap and Value Analyses in Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Pietro","family":"Ferrara","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)"},{"issue":"5-6","key":"17_CR2","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of PLDI 2003. ACM (2003)","DOI":"10.1145\/781151.781153"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 1\u201322. Springer, Heidelberg (2012)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-30579-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 147\u2013163. Springer, Heidelberg (2005)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Festschrift for Dave Schmidt, EPTCS (2013)","DOI":"10.4204\/EPTCS.129.11"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-642-24559-6_34","volume-title":"Formal Methods and Software Engineering","author":"G. Costantini","year":"2011","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 505\u2013521. Springer, Heidelberg (2011)"},{"key":"17_CR9","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: Proceedings of POPL 1977. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL 1979. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"17_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. Journal of Logic Programming\u00a013, 103\u2013179 (1992)","journal-title":"Journal of Logic Programming"},{"key":"17_CR12","unstructured":"Ferrara, P.: JAIL: Firewall analysis of java card by abstract interpretation. In: Proceedings of EAAI 2006 (2006)"},{"key":"17_CR13","unstructured":"Ferrara, P.: A fast and precise analysis for data race detection. In: Bytecode 2008 (2008)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-642-13464-7_15","volume-title":"Formal Techniques for Distributed Systems","author":"P. Ferrara","year":"2010","unstructured":"Ferrara, P.: Static type analysis of pattern matching by abstract interpretation. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE 2010, Part II. LNCS, vol.\u00a06117, pp. 186\u2013200. Springer, Heidelberg (2010)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-33826-7_5","volume-title":"Software Engineering and Formal Methods","author":"P. Ferrara","year":"2012","unstructured":"Ferrara, P., Fuchs, R., Juhasz, U.: TVAL+: TVLA and value analyses together. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 63\u201377. Springer, Heidelberg (2012)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Ferrara, P., Fuchs, R., Juhasz, U.: Tval+: A sound and generic combination of tvla and value analyses. Technical report, ETH Zurich (November 2013)","DOI":"10.1007\/978-3-642-33826-7_5"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-27940-9_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Ferrara","year":"2012","unstructured":"Ferrara, P., M\u00fcller, P.: Automatic inference of access permissions. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 202\u2013218. Springer, Heidelberg (2012)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-24730-2_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 512\u2013529. Springer, Heidelberg (2004)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proceedings of PLDI 2006. ACM (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Proceedings of PASTE 2001. ACM (2001)","DOI":"10.1145\/379605.379665"},{"issue":"2","key":"17_CR21","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: On affine relationships among variables of a program. Acta Informatica\u00a06(2), 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M. F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-74061-2_26","volume-title":"Static Analysis","author":"S. Magill","year":"2007","unstructured":"Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 419\u2013436. Springer, Heidelberg (2007)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15769-1_6","volume-title":"Static Analysis","author":"B. McCloskey","year":"2010","unstructured":"McCloskey, B., Reps, T., Sagiv, M.: Statically inferring complex heap, array, and numeric invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 71\u201399. Springer, Heidelberg (2010)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Might, M., Smaragdakis, Y., Van Horn, D.: Resolving and exploiting the k-cfa paradox: illuminating functional vs. object-oriented program analysis. In: Proceedings of PLDI 2010. ACM (2010)","DOI":"10.1145\/1806596.1806631"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded c programs with union types and pointer arithmetics. In: Proceedings of LCTES 2006. ACM (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation (2006)","DOI":"10.1007\/s10990-006-8609-1"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-35308-6_5","volume-title":"Certified Programs and Proofs","author":"V. Robert","year":"2012","unstructured":"Robert, V., Leroy, X.: A formally-verified alias analysis. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 11\u201326. Springer, Heidelberg (2012)"},{"issue":"3","key":"17_CR30","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-36946-9_8","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"M. Sridharan","year":"2013","unstructured":"Sridharan, M., Chandra, S., Dolby, J., Fink, S.J., Yahav, E.: Alias analysis for object-oriented programs. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol.\u00a07850, pp. 196\u2013232. Springer, Heidelberg (2013)"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A. Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol.\u00a01145, pp. 366\u2013382. Springer, Heidelberg (1996)"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-540-69149-5_24","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Venet","year":"2008","unstructured":"Venet, A.: Towards the integration of symbolic and numerical static analysis. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 227\u2013236. Springer, Heidelberg (2008)"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Zanioli, M., Ferrara, P., Cortesi, A.: SAILS: static analysis of information leakage with Sample. In: Proceedings of SAC 2012. ACM (2012)","DOI":"10.1145\/2245276.2231983"}],"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-642-54013-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,5]],"date-time":"2019-08-05T19:03:21Z","timestamp":1565031801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}