In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching

  • Dirk Beyer
  • Karlheinz Friedberger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, block summarization can be combined with counterexample-guided abstraction refinement (CEGAR). This causes the following problem: whenever CEGAR instructs the model checker to refine the abstraction along a path, several block summaries are affected and need to be updated. There exist two different refinement strategies: a destructive in-place approach that modifies the existing block abstractions and a constructive copy-on-write approach that does not change existing data. While the in-place approach is used in the field for several years, our new approach of copy-on-write refinement has the following important advantage: A complete exportable proof of the program is available after the analysis has finished. Due to the benefit from avoiding recomputations of missing information as necessary for in-place updates, the new approach causes almost no computational overhead overall. We perform a large experimental evaluation to compare the new approach with the previous one to show that full proofs can be achieved without overhead.


Software model checking Block summarization Copy-on-write CEGAR Abstraction refinement CPAchecker Program analysis 


  1. 1.
    Andrianov, P., Friedberger, K., Mandrykin, M.U., Mutilin, V.S., Volkov, A.: CPABAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. In: Proc. TACAS. LNCS, vol. 10206, pp. 355–359. Springer (2017)Google Scholar
  2. 2.
    Andrianov, P., Mutilin, V.S., Mandrykin, M.U., Vasilyev, A.: CPA-BAM-Slicing: Block-abstraction memoization and slicing with region-based dependency analysis (competition contribution). In: Proc. TACAS. LNCS, vol. 10806, pp. 427–431. Springer (2018)Google Scholar
  3. 3.
    Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proc. SPIN. LNCS, vol. 1885, pp. 113–130. Springer (2000)Google Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1–3. ACM (2002)Google Scholar
  5. 5.
    Beyer, D.: Software verification with validation of results (Report on SV-COMP 2017). In: Proc. TACAS. LNCS, vol. 10206, pp. 331–349. Springer (2017)Google Scholar
  6. 6.
    Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proc. FSE, pp. 326–337. ACM (2016)Google Scholar
  7. 7.
    Beyer, D., Friedberger, K.: Domain-independent multi-threaded software model checking. In: Proc. ASE, pp. 634–644. ACM (2018)Google Scholar
  8. 8.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5–6), 505–525 (2007)CrossRefGoogle Scholar
  9. 9.
    Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29–38. IEEE (2008)Google Scholar
  10. 10.
    Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. LNCS, vol. 6806, pp. 184–190. Springer (2011)Google Scholar
  11. 11.
    Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189–197. FMCAD (2010)Google Scholar
  12. 12.
    Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE. LNCS, vol. 7793, pp. 146–162. Springer (2013)Google Scholar
  13. 13.
    Beyer, D., Löwe, S., Wendler, P.: Refinement selection. In: Proc. SPIN. LNCS, vol. 9232, pp. 20–38. Springer (2015)Google Scholar
  14. 14.
    Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388–402 (2004)CrossRefGoogle Scholar
  15. 15.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Clarke, E.M., Kröning, D., Sharygina, N., Yorav, K.: SatAbs: SAT-based predicate abstraction for ANSI-C. In: Proc. TACAS. LNCS, vol. 3440, pp. 570–574. Springer (2005)Google Scholar
  17. 17.
    Friedberger, K.: CPA-BAM: Block-abstraction memoization with value analysis and predicate analysis. In: Proc. TACAS. LNCS, vol. 9636, pp. 912–915. Springer (2016)Google Scholar
  18. 18.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proc. PLDI, pp. 1–13. ACM (2004)Google Scholar
  19. 19.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58–70. ACM (2002)Google Scholar
  20. 20.
    Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Languages, pp. 102–116. Springer (1971)Google Scholar
  21. 21.
    Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the Swarm tool. In: Proc. SPIN 2008. LNCS, vol. 5156, pp. 134–143. Springer (2008)Google Scholar
  22. 22.
    McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119–161 (2011)CrossRefGoogle Scholar
  23. 23.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV. LNCS, vol. 4144, pp. 123–136. Springer (2006)Google Scholar
  24. 24.
    Reps, T.W.: Program analysis via graph reachability. In: Proc. ILPS, pp. 5–19. MIT (1997)Google Scholar
  25. 25.
    Sery, O., Fedyukovich, G., Sharygina, N.: Funfrog: Bounded model checking with interpolation-based function summarization. In: Proc. ATVA. LNCS, vol. 7561, pp. 203–207. Springer (2012)Google Scholar
  26. 26.
    Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Proc. HVC. LNCS, vol. 7261, pp. 160–175. Springer (2012)Google Scholar
  27. 27.
    Wonisch, D., Wehrheim, H.: Predicate analysis with block-abstraction memoization. In: Proc. ICFEM. LNCS, vol. 7635, pp. 332–347. Springer (2012)Google Scholar
  28. 28.
    Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using boolean satisfiability. TOPLAS 29(3), 16 (2007)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Dirk Beyer
    • 1
  • Karlheinz Friedberger
    • 1
  1. 1.LMU MunichMunichGermany

Personalised recommendations