Advertisement

Quantifiers on Demand

  • Arie GurfinkelEmail author
  • Sharon Shoham
  • Yakir Vizel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, Quic3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, Quic3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While Quic3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented Quic3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying Quic3 to verifying a variety of public benchmarks of array manipulating C programs.

Notes

Acknowledgments

This publication is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102-SVIS]). The research was partially supported by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, and the United States-Israel Binational Science Foundation (BSF) grants No. 2016260 and 2012259. We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC), RGPAS-2017-507912.

References

  1. 1.
    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: CAV (2012)Google Scholar
  2. 2.
    Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: ATVA (2014)Google Scholar
  3. 3.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: TACAS (2001)CrossRefGoogle Scholar
  4. 4.
    Beyer, D.: Software verification with validation of results. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 331–349. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54580-5_20CrossRefGoogle Scholar
  5. 5.
    Bjørner, Nikolaj, Gurfinkel, Arie: Property Directed Polyhedral Abstraction. In: D’Souza, Deepak, Lal, Akash, Larsen, Kim Guldstrand (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46081-8_15Google Scholar
  6. 6.
    Bjørner, N., Janota, M.: Playing with quantified satisfaction. In: LPAR (2015)Google Scholar
  7. 7.
    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
  8. 8.
    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
  9. 9.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2006)Google Scholar
  10. 10.
    Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Logical Methods Comput. Sci. 8(2) (2012)Google Scholar
  11. 11.
    Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: FMCAD (2013)Google Scholar
  12. 12.
    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
  13. 13.
    Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: European Symposium on Programming (ESOP) (2010)Google Scholar
  14. 14.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL (2002)Google Scholar
  15. 15.
    Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Computer Aided Verification (CAV) (2009)CrossRefGoogle Scholar
  16. 16.
    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
  17. 17.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV’97 (1997)CrossRefGoogle Scholar
  18. 18.
    Gurfinkel, A., Ivrii, A.: Pushing to the top. In: FMCAD (2015)Google Scholar
  19. 19.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Computer Aided Verification (CAV) (2015)Google Scholar
  20. 20.
    Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: FSE (2016)Google Scholar
  21. 21.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31612-8_13CrossRefGoogle Scholar
  22. 22.
    Hoder, K., Bjørner, N., de Moura, L.: \({\mu \text{ Z }}\)– an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457–462. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_36CrossRefGoogle Scholar
  23. 23.
    Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: CAV (2015)Google Scholar
  24. 24.
    Komuravelli, A., Bjørner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: FMCAD (2015)Google Scholar
  25. 25.
    Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Computer Aided Verification (CAV). Springer, Berlin (2014)Google Scholar
  26. 26.
    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
  27. 27.
    Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_11CrossRefzbMATHGoogle Scholar
  28. 28.
    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
  29. 29.
    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_18CrossRefGoogle Scholar
  30. 30.
    Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 260–276. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_17CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of WaterlooWaterlooCanada
  2. 2.Tel Aviv UniversityTel AvivIsrael
  3. 3.The TechnionHaifaIsrael

Personalised recommendations