Predicate Abstraction for Program Verification

Safety and Termination
  • Ranjit Jhala
  • Andreas Podelski
  • Andrey Rybalchenko
Chapter

Abstract

We present basic principles of algorithms for the verification of safety and termination of programs. The algorithms call procedures on logical formulas in order to construct an abstraction and to refine an abstraction. The two underlying concepts are predicate abstraction and counterexample-guided abstraction refinement.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  2. 2.
    Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 203–213. ACM, New York (2001) Google Scholar
  3. 3.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5(1), 49–58 (2003) CrossRefGoogle Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000) Google Scholar
  5. 5.
    Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 1–3. ACM, New York (2002) Google Scholar
  6. 6.
    Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Jagannathan, S., Sewell, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 221–234. ACM, New York (2014) MATHGoogle Scholar
  7. 7.
    Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  8. 8.
    Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Formal Methods in Computer Aided Design (FMCAD), pp. 25–32. IEEE, Piscataway (2009) Google Scholar
  9. 9.
    Beyer, D., Gulwani, S., Schmidt, D.A.: Combining model checking and data-flow analysis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  10. 10.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  11. 11.
    Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 189–197. IEEE, Piscataway (2010) Google Scholar
  12. 12.
    Bjørner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  13. 13.
    Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  14. 14.
    Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 105–122. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  15. 15.
    Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Clarke, L.A., Dillon, L., Tichy, W.F. (eds.) Intl. Conf. on Software Engineering (ICSE), pp. 385–395. IEEE, Piscataway (2003) Google Scholar
  16. 16.
    Chamarthi, H.R., Dillinger, P.C., Manolios, P., Vroon, D.: The ACL2 Sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6605, pp. 291–295. Springer, Heidelberg (2011) MATHGoogle Scholar
  17. 17.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  18. 18.
    Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005) MATHGoogle Scholar
  19. 19.
    Clarke, E.M., Kurshan, R.P., Veith, H.: The localization reduction and counterexample-guided abstraction refinement. In: Manna, Z., Peled, D.A. (eds.) Essays in Memory of Amir Pnueli. LNCS, vol. 6200, pp. 61–71. Springer, Heidelberg (2010) Google Scholar
  20. 20.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 415–426. ACM, New York (2006) Google Scholar
  21. 21.
    Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  22. 22.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013) Google Scholar
  23. 23.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 238–252. ACM, New York (1977) Google Scholar
  24. 24.
    Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Field, J., Hicks, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 245–258. ACM, New York (2012) Google Scholar
  25. 25.
    Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957) MathSciNetCrossRefGoogle Scholar
  26. 26.
    Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  27. 27.
    Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999) CrossRefGoogle Scholar
  28. 28.
    Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 271–274. Springer, Heidelberg (2010) Google Scholar
  29. 29.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) Intl. Symp. on Formal Methods Europe (FME). LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001) Google Scholar
  30. 30.
    Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, pp. 19–32. AMS, Providence (1967) CrossRefGoogle Scholar
  31. 31.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  32. 32.
    Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 405–416. ACM, New York (2012) Google Scholar
  33. 33.
    Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp. 117–127. ACM, New York (2006) Google Scholar
  34. 34.
    Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Ball, T., Sagiv, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 331–344. ACM, New York (2011) Google Scholar
  35. 35.
    Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  36. 36.
    Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 471–482. ACM, New York (2010) Google Scholar
  37. 37.
    Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 6337, pp. 22–50. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  38. 38.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 232–244. ACM, New York (2004) Google Scholar
  39. 39.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 58–70. ACM, New York (2002) Google Scholar
  40. 40.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) CrossRefGoogle Scholar
  41. 41.
    Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using F-SOFT. In: International Conference on Computer Design (ICCD), pp. 297–308. IEEE, Piscataway (2005) Google Scholar
  42. 42.
    Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009) CrossRefGoogle Scholar
  43. 43.
    Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  44. 44.
    Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  45. 45.
    Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 573–578. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  46. 46.
    Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  47. 47.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Hankin, C., Schmidt, D. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 81–92. ACM, New York (2001) Google Scholar
  48. 48.
    Lee, W., Wang, B., Yi, K.: Termination analysis with algorithmic learning. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 88–104. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  49. 49.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  50. 50.
    Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi project: software property checking via static analysis and testing. In: Kowalewski, S., Philippou, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 5505, pp. 178–181. Springer, Heidelberg (2009) Google Scholar
  51. 51.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  52. 52.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: Symp. on Logic in Computer Science (LICS), pp. 32–41. IEEE, Piscataway (2004) Google Scholar
  53. 53.
    Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Palsberg, J., Abadi, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 132–144. ACM, New York (2005) Google Scholar
  54. 54.
    Podelski, A., Rybalchenko, A.A.: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) Practical Aspects of Declarative Languages (PADL). LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  55. 55.
    Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 3672, pp. 268–283. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  56. 56.
    Podelski, A., Wies, T.: Counterexample-guided focus. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 249–260. ACM, New York (2010) Google Scholar
  57. 57.
    Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 159–169. ACM, New York (2008) Google Scholar
  58. 58.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Ranjit Jhala
    • 1
  • Andreas Podelski
    • 2
  • Andrey Rybalchenko
    • 3
  1. 1.Jacobs School of EngineeringUniversity of California, San DiegoSan DiegoUSA
  2. 2.University of FreiburgFreiburgGermany
  3. 3.Microsoft ResearchCambridgeUK

Personalised recommendations