Abstract
Effective static analyses must precisely approximate both heap structure and information about values. During the last decade, shape analysis has obtained great achievements in the field of heap abstraction. Similarly, numerical and other value abstractions have made tremendous progress, and they are effectively applied to the analysis of industrial software. In addition, several generic static analyzers have been introduced. These compositional analyzers combine many types of abstraction into the same analysis to prove various properties. The main contribution of this paper is the combination of Sample, an existing generic analyzer, with a TVLA-based heap abstraction (TVAL+).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5-6), 505–525 (2007)
Beyer, D., Henzinger, T.A., Théoduloz, G.: Lazy Shape Analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 532–546. Springer, Heidelberg (2006)
Bouajjani, A., Drăgoi, 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. 7148, pp. 1–22. Springer, Heidelberg (2012)
Costantini, G., Ferrara, P., Cortesi, A.: Static Analysis of String Values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 505–521. Springer, Heidelberg (2011)
Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)
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)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL 1979. ACM Press (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL 1978. ACM Press (1978)
Fähndrich, M., Logozzo, F.: Static Contract Checking with Abstract Interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011)
Ferrara, P.: Checkmate: a generic static analyzer of java multithreaded programs. In: Proceedings of SEFM 2009. IEEE Computer Society Press (2009)
Ferrara, P.: Static Type Analysis of Pattern Matching by Abstract Interpretation. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010, Part II. LNCS, vol. 6117, pp. 186–200. Springer, Heidelberg (2010)
Ferrara, P., Müller, P.: Automatic Inference of Access Permissions. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 202–218. Springer, Heidelberg (2012)
Gabi, D.: Disjunction on demand. Master thesis, ETH Zürich (2011)
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. 2988, pp. 512–529. Springer, Heidelberg (2004)
Gopan, D., Reps, T.W., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of POPL 2005. ACM Press (2005)
Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proceedings of PLDI 2006. ACM Press (2006)
Jeannet, B., Miné, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)
Lev-Ami, T., Sagiv, M.: TVLA: A framework for kleene logic based static analyses. Master’s thesis, Tel Aviv University (2000)
Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic Strengthening for Shape Analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 419–436. Springer, Heidelberg (2007)
Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
McCloskey, B., Reps, T., Sagiv, M.: Statically Inferring Complex Heap, Array, and Numeric Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 71–99. Springer, Heidelberg (2010)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation (2006)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Spoto, F.: Julia: A Generic Static Analyser for the Java Bytecode. In: Proceedings of FTfJP 2004 (2005)
Zanioli, M., Ferrara, P., Cortesi, A.: SAILS: static analysis of information leakage with Sample. In: Proceedings of SAC 2012. ACM Press (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrara, P., Fuchs, R., Juhasz, U. (2012). TVAL+ : TVLA and Value Analyses Together. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)