×

Loop summarization using abstract transformers. (English) Zbl 1183.68377

Cha, Sungdeok (Steve) (ed.) et al., Automated technology for verification and analysis. 6th international symposium, ATVA 2008, Seoul, Korea, October 20–23, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-88386-9/pbk). Lecture Notes in Computer Science 5311, 111-125 (2008).
Summary: Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.
For the entire collection see [Zbl 1148.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Calysto; CSSV; CBMC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977) · doi:10.1145/512950.512973
[2] Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84–96 (1978) · doi:10.1145/512760.512770
[3] Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992) · Zbl 0776.68024 · doi:10.1007/3-540-55844-6_142
[4] Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004) · Zbl 1202.68255 · doi:10.1007/978-3-540-24622-0_21
[5] Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD 25, 105–127 (2004) · Zbl 1090.68022
[6] Gopan, D., Reps, T.W.: Low-level library analysis and summarization. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 68–81. Springer, Heidelberg (2007) · Zbl 05216215 · doi:10.1007/978-3-540-73368-3_10
[7] Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: theory and applications. Prentice-Hall, Englewood Cliffs (1981)
[8] Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: PASTE, pp. 43–48. ACM, New York (2007) · doi:10.1145/1251535.1251543
[9] Babic, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: ICSE, pp. 211–220. ACM, New York (2008) · doi:10.1145/1368088.1368118
[10] Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, pp. 14–25 (2000) · doi:10.1145/347324.383378
[11] Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004) · Zbl 1126.68470 · doi:10.1007/978-3-540-24730-2_15
[12] Clarke, E., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
[13] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979) · Zbl 1323.68356 · doi:10.1145/567752.567778
[14] Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) · doi:10.1007/3-540-63166-6_10
[15] Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 24–38. Springer, Heidelberg (2005) · Zbl 1081.68055 · doi:10.1007/11513988_5
[16] Kroening, D., Sharygina, N.: Approximating predicate images for bit-vector logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 242–256. Springer, Heidelberg (2006) · Zbl 1180.68175 · doi:10.1007/11691372_16
[17] Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006) · Zbl 05187390 · doi:10.1007/11817963_39
[18] Cavada, R., Cimatti, A., Franzén, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD, pp. 69–76. IEEE, Los Alamitos (2007)
[19] Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28, 594–614 (1981) · Zbl 0462.68042 · doi:10.1145/322261.322273
[20] Ashcroft, E., Manna, Z.: The translation of ’go to’ programs to ’while’ programs, pp. 49–61 (1979)
[21] Dor, N., Rodeh, M., Sagiv, S.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI, pp. 155–167 (2003) · doi:10.1145/781131.781149
[22] Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. In: SIGSOFT FSE, pp. 97–106 (2004) · doi:10.1145/1029894.1029911
[23] Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: ASE 2007, pp. 389–392. ACM Press, New York (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.