Advertisement

Cluster Computing

, Volume 22, Supplement 3, pp 6219–6229 | Cite as

An improved method of k-induction combined with predicate abstraction and CEGAR for software model checking

  • Shun Wang
  • Ye DuEmail author
  • Zhen Han
Article
  • 44 Downloads

Abstract

K-induction and predicate abstraction are well known techniques for unbounded software model checking. However, these methods are always treated as completely different in previous works. In the paper, we develop a combined method that merges k-induction and predicate abstraction into a CEGAR-based general abstraction method, which divides the target program into blocks that can be explored separately and extends k-induction in an abstract domain. Experiment results show that the combined method balances effectiveness and efficiency on k-induction and predicate abstraction implementations.

Keywords

Abstract-refinement Software model checking Optimization algorithm Predicate analysis Interpolation Shape analysis 

References

  1. 1.
    Clarke, E., Grumberg, O., Jha, S.: Counterexample-guided abstraction refinement. In: Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, USA, pp. 154–169 (2000)Google Scholar
  2. 2.
    Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 752–769 (2016)Google Scholar
  3. 3.
    Prabhakar, P., Soto, M.G.: Counterexample guided abstraction refinement for stability analysis. In: Proceedings of the 28th International Conference on Computer Aided Verification, Toronto, Canada, pp. 495–512 (2016)Google Scholar
  4. 4.
    Hajdu, Á., Tóth, T., Vörös, A., et al.: A configurable CEGAR framework with interpolation-based refinements. In: 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 158–174. Springer, Heidelberg (2016)CrossRefGoogle Scholar
  5. 5.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. Comput. Sci. 6806, 184–190 (2011)MathSciNetGoogle Scholar
  6. 6.
    Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker, with sequential combination of explicit-value analyses and predicate analyses. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 392–394. Springer, Berlin (2014)CrossRefGoogle Scholar
  7. 7.
    Friedberger, K.: CPA-BAM: block-abstraction memorization with value analysis and predicate analysis. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Netherlands, pp. 912–915 (2016)Google Scholar
  8. 8.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, USA, pp. 70–87 (2011)Google Scholar
  9. 9.
    Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proceedings of the 26th International Conference on Computer Aided Verification, Vienna, Austria, pp. 831–848 (2014)CrossRefGoogle Scholar
  10. 10.
    Cimatti, A., Griggio, A., Mover, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Form. Methods Syst. Des. 49(3), 190–218 (2016)CrossRefGoogle Scholar
  11. 11.
    Günther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 954–957 (2016)Google Scholar
  12. 12.
    Rocha, W., Rocha, H., Ismail, H.: DepthK: A k-induction verifier based on invariant inference for C programs. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Greece, pp. 360–364 (2017)Google Scholar
  13. 13.
    Karpenkov, E.G.: LPI: software verification with local policy iteration. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 930–933 (2016)Google Scholar
  14. 14.
    Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proceedings of the 27th International Conference on Computer Aided Verification, California, USA, pp. 622–640 (2015)Google Scholar
  15. 15.
    Kahsai, T., Tinelli, C.: Pkind: a parallel k-induction based model checker. Electronic Proceedings in Theoretical Computer Science 72, 55–62 (2011)CrossRefGoogle Scholar
  16. 16.
    Hickey, R.: The Clojure programming language. In: Proceedings of the 2008 Symposium on Dynamic languages, Cyprus, p. 1 (2008)Google Scholar
  17. 17.
    Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Proceedings of the 19th International Conference on Model Checking Software, Oxford, UK, pp. 248–254 (2012)Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2018

Authors and Affiliations

  1. 1.School of Computer and Information TechnologyBeijing Jiaotong UniversityBeijingChina

Personalised recommendations