×

zbMATH — the first resource for mathematics

Whale: an interpolation-based algorithm for inter-procedural verification. (English) Zbl 1325.68137
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 39-55 (2012).
Summary: In software verification, Craig interpolation has proven to be a powerful technique for computing and refining abstractions. In this paper, we propose an interpolation-based software verification algorithm for checking safety properties of (possibly recursive) sequential programs. Our algorithm, called Whale, produces inter-procedural proofs of safety by exploiting interpolation for guessing function summaries by generalizing under-approximations (i.e., finite traces) of functions. We implemented our algorithm in LLVM and applied it to verifying properties of low-level code written for the pacemaker challenge. We show that our prototype implementation outperforms existing state-of-the-art tools.
For the entire collection see [Zbl 1236.68007].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale Homepage, http://www.cs.toronto.edu/ aws/whale
[2] Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001) · Zbl 0978.68540 · doi:10.1007/3-540-45319-9_19
[3] Ball, T., Rajamani, S.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001) · Zbl 0996.68560 · doi:10.1007/3-540-44585-4_25
[4] Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast. STTT 9(5-6), 505–525 (2007) · Zbl 05536156 · doi:10.1007/s10009-007-0044-z
[5] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008) · Zbl 05301118 · doi:10.1007/978-3-540-70545-1_28
[6] Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. ACM Trans. Comput. Log. 12(1), 7 (2010) · Zbl 1351.68247 · doi:10.1145/1838552.1838559
[7] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000) · Zbl 0974.68517 · doi:10.1007/10722167_15
[8] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
[9] Craig, W.: Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. The Journal of Symbolic Logic 22(3), 269–285 (1957) · Zbl 0079.24502 · doi:10.2307/2963594
[10] Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM TOPLAS 13(4), 451–490 (1991) · doi:10.1145/115372.115320
[11] Godefroid, P., Nori, A., Rajamani, S., Tetali, S.: Compositional Must Program Analysis: Unleashing the Power of Alternation. In: Proc. of POPL 2010, pp. 43–56 (2010) · Zbl 1312.68057 · doi:10.1145/1706299.1706307
[12] 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
[13] Gulavani, B., Henzinger, T., Kannan, Y., Nori, A., Rajamani, S.: SYNERGY: a New Algorithm for Property Checking. In: Robshaw, M.J.B. (ed.) FSE 2006. LNCS, vol. 4047, pp. 117–127. Springer, Heidelberg (2006) · doi:10.1145/1181775.1181790
[14] Gurfinkel, A., Chaki, S., Sapra, S.: Efficient Predicate Abstraction of Program Summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 131–145. Springer, Heidelberg (2011) · Zbl 05930525 · doi:10.1007/978-3-642-20398-5_11
[15] Gurfinkel, A., Wei, O., Chechik, M.: Yasm: A Software Model-Checker for Verification and Refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170–174. Springer, Heidelberg (2006) · Zbl 05187427 · doi:10.1007/11817963_18
[16] Heizmann, M., Hoenicke, J., Podelski, A.: Nested Interpolants. In: Proc. of POPL 2010, pp. 471–482 (2010) · Zbl 1312.68059 · doi:10.1145/1706299.1706353
[17] Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. of POPL 2002, pp. 58–70 (2002) · Zbl 1323.68374 · doi:10.1145/503272.503279
[18] Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: Proc. of POPL 2004, pp. 232–244 (2004) · Zbl 1325.68147 · doi:10.1145/964001.964021
[19] Hoare, C.: Procedures and Parameters: An Axiomatic Approach. In: Proc. of Symp. on Semantics of Algorithmic Languages, vol. 188, pp. 102–116 (1971) · Zbl 0221.68020 · doi:10.1007/BFb0059696
[20] Hoare, C.: An Axiomatic Basis for Computer Programming. Comm. ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[21] Jhala, R., McMillan, K.L.: Interpolant-Based Transition Relation Approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005) · Zbl 1081.68622 · doi:10.1007/11513988_6
[22] Kroening, D., Weissenbacher, G.: Interpolation-Based Software Verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 573–578. Springer, Heidelberg (2011) · Zbl 05940743 · doi:10.1007/978-3-642-22110-1_45
[23] Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proc. of CGP 2004 (March 2004) · doi:10.1109/CGO.2004.1281665
[24] Manna, Z., McCarthy, J.: Properties of Programs and Partial Function Logic. J. of Machine Intelligence 5 (1970) · Zbl 0221.68016
[25] McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1
[26] McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010) · Zbl 05772623 · doi:10.1007/978-3-642-14295-6_10
[27] McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) · Zbl 1188.68196 · doi:10.1007/11817963_14
[28] Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall (1981)
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.