{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T12:15:31Z","timestamp":1725624931800},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642338250"},{"type":"electronic","value":"9783642338267"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_5","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"63-77","source":"Crossref","is-referenced-by-count":11,"title":["TVAL+ : TVLA and Value Analyses Together"],"prefix":"10.1007","author":[{"given":"Pietro","family":"Ferrara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raphael","family":"Fuchs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uri","family":"Juhasz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5-6","key":"5_CR1","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":"5_CR2","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":"5_CR3","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":"5_CR4","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":"5_CR5","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"5_CR6","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 Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL 1979. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL 1978. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"5_CR9","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":"5_CR10","doi-asserted-by":"crossref","unstructured":"Ferrara, P.: Checkmate: a generic static analyzer of java multithreaded programs. In: Proceedings of SEFM 2009. IEEE Computer Society Press (2009)","DOI":"10.1109\/SEFM.2009.20"},{"key":"5_CR11","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 2010, Part II. LNCS, vol.\u00a06117, pp. 186\u2013200. Springer, Heidelberg (2010)"},{"key":"5_CR12","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":"5_CR13","unstructured":"Gabi, D.: Disjunction on demand. Master thesis, ETH Z\u00fcrich (2011)"},{"key":"5_CR14","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":"5_CR15","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of POPL 2005. ACM Press (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proceedings of PLDI 2006. ACM Press (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"5_CR17","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.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"5_CR18","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A framework for kleene logic based static analyses. Master\u2019s thesis, Tel Aviv University (2000)"},{"key":"5_CR19","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":"5_CR20","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":"5_CR21","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":"5_CR22","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"},{"issue":"3","key":"5_CR23","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. TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"5_CR24","unstructured":"Spoto, F.: Julia: A Generic Static Analyser for the Java Bytecode. In: Proceedings of FTfJP 2004 (2005)"},{"key":"5_CR25","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 Press (2012)","DOI":"10.1145\/2245276.2231983"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:22:16Z","timestamp":1620130936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}