×

Predicate abstraction for program verification. (English) Zbl 1392.68253

Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 447-491 (2018).
Summary: 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.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

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) · doi:10.1007/978-3-642-31424-7_48
[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)
[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) · Zbl 0978.68540 · doi:10.1007/s10009-002-0095-0
[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) · Zbl 0976.68540
[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)
[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) · Zbl 1284.91009
[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) · doi:10.1007/978-3-642-39799-8_61
[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)
[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) · Zbl 1392.68231
[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) · doi:10.1007/978-3-642-22110-1_16
[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)
[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) · doi:10.1007/978-3-642-38856-9_8
[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) · doi:10.1007/978-3-642-39799-8_28
[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) · doi:10.1007/978-3-642-31424-7_13
[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)
[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) · Zbl 1316.68132
[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) · Zbl 0974.68517 · doi:10.1007/10722167_15
[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) · Zbl 1087.68586
[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)
[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)
[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) · doi:10.1007/11817963_37
[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) · Zbl 1381.68050
[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)
[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) · Zbl 1321.68190
[25] 25. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250-268 (1957) · Zbl 0081.24402 · doi:10.2307/2963593
[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) · Zbl 1392.68244
[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) · Zbl 1046.68589 · doi:10.1007/3-540-48683-6_16
[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)
[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) · Zbl 0977.68671
[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) · Zbl 0189.50204 · doi:10.1090/psapm/019/0235771
[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) · doi:10.1007/3-540-63166-6_10
[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)
[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)
[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) · Zbl 1284.68427
[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) · doi:10.1007/978-3-642-22110-1_32
[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) · Zbl 1312.68059
[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) · Zbl 1306.68028 · doi:10.1007/978-3-642-15769-1_4
[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) · Zbl 1325.68147
[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) · Zbl 1323.68374
[40] 40. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[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)
[42] 42. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1-21:54 (2009) · Zbl 1507.68188 · doi:10.1145/1592434.1592438
[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) · Zbl 1135.68474 · doi:10.1007/978-3-540-73368-3_23
[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) · doi:10.1007/978-3-642-14295-6_9
[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) · doi:10.1007/978-3-642-22110-1_45
[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) · Zbl 1103.68627 · doi:10.1007/978-3-540-27813-9_11
[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) · Zbl 1323.68216
[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) · doi:10.1007/978-3-642-31424-7_12
[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) · Zbl 1188.68196 · doi:10.1007/11817963_14
[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)
[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) · Zbl 1202.68109 · doi:10.1007/978-3-540-24622-0_20
[52] 52. Podelski, A., Rybalchenko, A.: Transition invariants. In: Symp. on Logic in Computer Science (LICS), pp. 32-41. IEEE, Piscataway (2004) · Zbl 1315.68104
[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) · Zbl 1369.68152
[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) · doi:10.1007/978-3-540-69611-7_16
[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) · Zbl 1141.68374 · doi:10.1007/11547662_19
[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) · Zbl 1312.68067
[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) · Zbl 1312.68033
[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) · doi:10.1145/514188.514190
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.