Invariants synthesis over a combined domain for automated program verification. (English) Zbl 1390.68190

Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 304-325 (2013).
Summary: Program invariants such as loop invariants and method specifications (a.k.a. procedural summaries) are key components in program verification. Such invariants are usually manually specified by users before passed as inputs to a program verifier. The process of manually annotating programs with such invariants is tedious and error-prone and can significantly hinder the level of automation in program verification. Although invariant synthesis techniques have made noticeable progress in reducing the burden of user annotations; when it comes to automated verification of memory safety and functional correctness for heap-manipulating programs, it remains a rather challenging task to discover program specifications and invariants automatically, due to the complexity of aliasing and mutability of data structures.
In this paper, we present invariant synthesis algorithms for the following scenarios: i) to synthesise a missing loop invariant, ii) to refine given pre/post shape templates to complete pre/post-conditions, iii) to infer a missing precondition, iv) to calculate a missing postcondition, given a precondition. The proposed analyses are based on abstract interpretation and are built over an abstract domain combining separation, numerical and multi-set (bag) information. Our inference mechanisms are equipped with newly designed abstraction, join, widening and abduction operations. Initial prototypical experiments have shown that they are viable and powerful enough to discover interesting useful invariants for non-trivial programs.
For the entire collection see [Zbl 1269.68023].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI


[1] Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4 (2005) · Zbl 02243139
[2] Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006) · Zbl 05189652
[3] Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
[4] Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007) · Zbl 1135.68466
[5] Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: On inter-procedural analysis of programs with lists and data. In: PLDI (2011)
[6] 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) · Zbl 1325.68058
[7] Bozga, M., Iosif, R., Lakhnech, Y.: Storeless semantics and alias logic. In: PEPM (2003)
[8] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009) · Zbl 1315.68085
[9] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6) (2011) · Zbl 1281.68155
[10] Chang, B.Y.E., Rival, X.: Relational inductive shape analysis. In: POPL (2008) · Zbl 1295.68081
[11] Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. of Comp. Prog. 77 (2012) · Zbl 1243.68148
[12] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1977) · Zbl 1149.68389
[13] Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond -limiting. In: PLDI (1994)
[14] Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006) · Zbl 1180.68112
[15] Filliâtre, J.-C., Paskevich, A.: Why3 – where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013) · Zbl 1435.68366
[16] Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006) · Zbl 1225.68072
[17] Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Shao, Z., Pierce, B.C. (eds.) POPL (2009) · Zbl 1315.68094
[18] Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI (2007)
[19] Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005) · Zbl 1369.68140
[20] Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL (2001) · Zbl 1323.68077
[21] Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for c and java. In: NASA Formal Methods (2011) · Zbl 05930518
[22] Jonkers, H.: Abstract storage structures. Algorithmic Languages (1981) · Zbl 0463.68028
[23] Kuncak, V., Lam, P., Rinard, M.C.: Role analysis. In: POPL (2002) · Zbl 1323.68378
[24] Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL (2008) · Zbl 1295.68087
[25] Laviron, V., Chang, B.-Y.E., Rival, X.: Separating shape graphs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 387–406. Springer, Heidelberg (2010) · Zbl 1260.68103
[26] Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009) · Zbl 05619517
[27] Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: THOR: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 428–432. Springer, Heidelberg (2008) · Zbl 05301131
[28] Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: POPL (2010) · Zbl 1312.68063
[29] Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007) · Zbl 1132.68477
[30] Pham, T.-H., Trinh, M.-T., Truong, A.-H., Chin, W.-N.: FixBag: A fixpoint calculator for quantified bag constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 656–662. Springer, Heidelberg (2011) · Zbl 05940751
[31] Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2008) · Zbl 05252984
[32] Qin, S., He, G., Luo, C., Chin, W.-N.: Loop invariant synthesis in a combined domain. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 468–484. Springer, Heidelberg (2010) · Zbl 05854665
[33] Qin, S., He, G., Luo, C., Chin, W.N., Chen, X.: Loop invariant synthesis in a combined abstract domain. J. Symb. Comput. 50 (2013) · Zbl 1256.68044
[34] Qin, S., He, G., Luo, C., Chin, W.N., Yang, H.: Automatically refining partial specifications for heap-manipulating programs. Sci. Comput. Program. (accepted to appear)
[35] Qin, S., Luo, C., Chin, W.-N., He, G.: Automatically refining partial specifications for program verification. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 369–385. Springer, Heidelberg (2011) · Zbl 05915262
[36] Rakamarić, Z., Bruttomesso, R., Hu, A.J., Cimatti, A.: Verifying heap-manipulating programs in an SMT framework. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 237–252. Springer, Heidelberg (2007) · Zbl 1141.68484
[37] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
[38] Rival, X., Chang, B.Y.E.: Calling context abstraction with shapes. In: POPL (2011) · Zbl 1284.68198
[39] Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI (2008) · Zbl 1312.68033
[40] Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: POPL (2010) · Zbl 1312.68033
[41] Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3) (2002) · Zbl 05459332
[42] Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008) · Zbl 1155.68359
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.