Advertisement

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

  • Oren Ish-ShalomEmail author
  • Shachar ItzhakyEmail author
  • Noam RinetzkyEmail author
  • Sharon ShohamEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11990)

Abstract

Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of inductive quantified loop invariants which, in some cases, may not even be first-order expressible. In this paper, we suggest a novel verification technique that is based on induction on user-defined rank of program states as an alternative to loop-invariants. Our technique, dubbed inductive rank reduction, works in two steps. Firstly, we simplify the verification problem and prove that the program is correct when the input state contains an input array of length \(\ell _\textsf {B}\) or less, using the length of the array as the rank of the state. Secondly, we employ a squeezing function \(\curlyvee \) which converts a program state \(\sigma \) with an array of length \(\ell > \ell _\textsf {B}\) to a state Open image in new window containing an array of length \(\ell -1\) or less. We prove that when \(\curlyvee \) satisfies certain natural conditions then if the program violates its specification on \(\sigma \) then it does so also on Open image in new window. The correctness of the program on inputs with arrays of arbitrary lengths follows by induction.

We make our technique automatic for array programs whose length of execution is proportional to the length of the input arrays by (i) performing the first step using symbolic execution, (ii) verifying the conditions required of \(\curlyvee \) using Z3, and (iii) providing a heuristic procedure for synthesizing \(\curlyvee \). We implemented our technique and applied it successfully to several interesting array-manipulating programs, including a bidirectional summation program whose loop invariant cannot be expressed in first-order logic while its specification is quantifier-free.

Notes

Acknowledgements

The research leading to these results has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. [759102-SVIS]), the Lev Blavatnik and the Blavatnik Family foundation, Blavatnik Interdisciplinary Cyber Research Center at Tel Aviv University, Pazy Foundation, Israel Science Foundation (ISF) grants No. 1996/18 and 1810/18, and the Binational Science Foundation (NSF-BSF) grant 2018675.

References

  1. 1.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27–30 July 1996, pp. 313–321 (1996).  https://doi.org/10.1109/LICS.1996.561359
  2. 2.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000).  https://doi.org/10.1006/inco.1999.2843MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476–495. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_28CrossRefzbMATHGoogle Scholar
  4. 4.
    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679–685. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_49CrossRefGoogle Scholar
  5. 5.
    Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18–23. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_2CrossRefzbMATHGoogle Scholar
  6. 6.
    Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software. Systems Engineering, vol. 40, pp. 1–25 (2015)Google Scholar
  7. 7.
    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).  https://doi.org/10.1007/3-540-45319-9_19CrossRefzbMATHGoogle Scholar
  8. 8.
    Bjørner, N., Ganesh, V., Michel, R., Veanes, M.: SMT-LIB sequences and regular expressions. In: 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, 30 June–1 July 2012, pp. 77–87 (2012)Google Scholar
  9. 9.
    Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38856-9_8CrossRefGoogle Scholar
  10. 10.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_7CrossRefGoogle Scholar
  11. 11.
    Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Log. Methods Comput. Sci. 8(2) (2012).  https://doi.org/10.2168/LMCS-8(2:4)2012
  12. 12.
    Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 209–224. USENIX Association, Berkeley (2008). http://dl.acm.org/citation.cfm?id=1855741.1855756
  13. 13.
    Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013).  https://doi.org/10.1145/2408776.2408795CrossRefGoogle Scholar
  14. 14.
    Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs by tiling. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 428–449. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66706-5_21CrossRefGoogle Scholar
  15. 15.
    Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 61–68 (2013). http://ieeexplore.ieee.org/document/6679392/
  16. 16.
    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, pp. 238–252. ACM Press, New York, Los Angeles (1977)Google Scholar
  17. 17.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  18. 18.
    Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000).  https://doi.org/10.1007/10721959_19CrossRefGoogle Scholar
  19. 19.
    Farzan, A., Nicolet, V.: Modular divide-and-conquer parallelization of nested loops. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 610–624. ACM, New York (2019).  https://doi.org/10.1145/3314221.3314612
  20. 20.
    Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Computer Aided Verification - Proceedings of the 31st International Conference, CAV 2019, New York City, NY, USA, 15–18 July 2019, Part I, pp. 259–277 (2019).  https://doi.org/10.1007/978-3-030-25540-4_14
  21. 21.
    Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: ACM SIGPLAN Notices. vol. 50, pp. 229–239. ACM (2015)Google Scholar
  22. 22.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001).  https://doi.org/10.1016/S0304-3975(00)00102-XMathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16–18 January 2002, pp. 191–202 (2002).  https://doi.org/10.1145/503272.503291
  24. 24.
    Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14203-1_3CrossRefGoogle Scholar
  25. 25.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63166-6_10CrossRefGoogle Scholar
  26. 26.
    Gulwani, S.: Programming by examples (and its applications in data wrangling). In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Verification and Synthesis of Correct and Secure Systems. IOS Press (2016)Google Scholar
  27. 27.
    Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13–18 November 2016, pp. 338–348 (2016).  https://doi.org/10.1145/2950290.2950330
  28. 28.
    Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248–266. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-01090-4_15CrossRefGoogle Scholar
  29. 29.
    Hua, J., Khurshid, S.: EdSketch: execution-driven sketching for Java. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 162–171. ACM (2017)Google Scholar
  30. 30.
    Itzhaky, S., et al.: Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 145–164. ACM (2016)Google Scholar
  31. 31.
    Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_55CrossRefGoogle Scholar
  32. 32.
    Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 583–602. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_40CrossRefGoogle Scholar
  33. 33.
    Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 213–231. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_12CrossRefGoogle Scholar
  34. 34.
    Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_22CrossRefGoogle Scholar
  35. 35.
    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).  https://doi.org/10.1007/11817963_14CrossRefGoogle Scholar
  36. 36.
    Miné, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31–100 (2006)CrossRefGoogle Scholar
  37. 37.
    Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361–382. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53413-7_18 CrossRefGoogle Scholar
  38. 38.
    Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. In: ACM SIGPLAN Notices. vol. 50, pp. 619–630. ACM (2015)Google Scholar
  39. 39.
    Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45319-9_7CrossRefGoogle Scholar
  40. 40.
    Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 38–49. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-03592-1_3CrossRefGoogle Scholar
  41. 41.
    Smith, C., Albarghouthi, A.: Mapreduce program synthesis. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 326–340. ACM (2016)Google Scholar
  42. 42.
    Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. ACM SIGOPS Oper. Syst. Rev. 40(5), 404–415 (2006)CrossRefGoogle Scholar
  43. 43.
    Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: ACM Sigplan Notices, vol. 45, pp. 313–326. ACM (2010)Google Scholar
  44. 44.
    Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. Int. J. Softw. Tools Technol. Transfer 15(5–6), 497–518 (2013) CrossRefGoogle Scholar
  45. 45.
    Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: TRANSIT: specifying protocols with concolic snippets. ACM SIGPLAN Not. 48(6), 287–296 (2013)CrossRefGoogle Scholar
  46. 46.
    Wang, C., Cheung, A., Bodik, R.: Synthesizing highly expressive SQL queries from input-output examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 452–466. ACM (2017)Google Scholar
  47. 47.
    Wang, K., Sullivan, A., Marinov, D., Khurshid, S.: Solver-based sketching of alloy models using test valuations. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 121–136. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91271-4_9CrossRefGoogle Scholar
  48. 48.
    Zuck, L.D., McMillan, K.L.: Invisible invariants are neither. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds.) From Reactive Systems to Cyber-Physical Systems. LNCS, vol. 11500, pp. 57–72. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-31514-6_5CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Tel Aviv UniversityTel AvivIsrael
  2. 2.TechnionHaifaIsrael

Personalised recommendations