×

Combining model checking and data-flow analysis. (English) Zbl 1392.68231

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). 493-540 (2018).
Summary: Until recently, model checking and data-flow analysis – two traditional approaches to software verification – were used independently and in isolation for solving similar problems. Theoretically, the two different approaches are equivalent; they are two different ways to compute the same solution to a problem. In recent years, new practical approaches have shown how to combine the approaches and how to make them benefit from each other – model-checking techniques can make data-flow analyses more precise, and data-flow-analysis techniques can make model checking more efficient. This chapter starts by discussing the relationship (differences and similarities) between type checking, data-flow analysis, and model checking. Then we define algorithms for data-flow analysis and model checking in the same formal setting, called configurable program analysis. This identifies key differences that make us call an algorithm a “model-checking” algorithm or a “data-flow-analysis” algorithm. We illustrate the effect of using different algorithms for running certain classic example analyses and point out the reason for one algorithm being “better” than the other. The chapter presents combined verification techniques in the framework of configurable program analysis, in order to emphasize techniques used in data-flow analysis and in model checking. Besides the iterative algorithm that is used to illustrate the similarities and differences between data-flow analysis and model checking, we discuss different algorithmic approaches for constructing program invariants. To show that the border between data-flow analysis and model checking is blurring and disappearing, we also discuss directions in tool implementations for combined verification approaches.
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. Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996) · Zbl 0876.68014
[2] 2. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986) · Zbl 1155.68020
[3] 3. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstractions for model checking C programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 268-283. Springer, Heidelberg (2001) · Zbl 0978.68540
[4] 4. Ball, T., Rajamani, S.K.: The
[5] 5. Ball, T., Rajamani, S.K.: SLIC: a specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2002)
[6] 6. Beyer, D.: Status report on software verification (competition summary SV-COMP 2014). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 373-388. Springer, Heidelberg (2014)
[7] 7. Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) Intl. Conf. on Software Engineering (ICSE), pp. 326-335. IEEE, Piscataway (2004)
[8] 8. Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The
[9] 9. 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)
[10] 10. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Intl. Symp. on Foundations of Software Engineering (FSE). ACM, New York (2016)
[11] 11. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp. 721-733. ACM, New York (2015)
[12] 12. Beyer, D., Fararooy, A.: A simple and effective measure for complex low-level dependencies. In: Intl. Conf. on Program Comprehension (ICPC), pp. 80-83. IEEE, Piscataway (2010)
[13] 13. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker
[14] 14. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 4349, pp. 378-394. Springer, Heidelberg (2007) · Zbl 1132.68333
[15] 15. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J., McKinley, K.S. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 300-309. ACM, New York (2007)
[16] 16. Beyer, D., Henzinger, T.A., Théoduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 532-546. Springer, Heidelberg (2006)
[17] 17. Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 504-518. Springer, Heidelberg (2007) · Zbl 1135.68466
[18] 18. Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Intl. Conf. on Automated Software Engineering (ASE), pp. 29-38. IEEE, Piscataway (2008)
[19] 19. Beyer, D., Henzinger, T.A., Théoduloz, G., Zufferey, D.: Shape refinement through explicit heap analysis. In: Rosenblum, D.S., Taentzer, G. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol. 6013, pp. 263-277. Springer, Heidelberg (2010)
[20] 20. Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Information reuse for multi-goal reachability analyses. In: Felleisen, M., Gardner, P. (eds.) European Symp. on Programming (ESOP). LNCS, vol. 7792, pp. 472-491. Springer, Heidelberg (2013) · Zbl 1381.68148
[21] 21. Beyer, D., Keremoglu, M.E.:
[22] 22. 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 (2010)
[23] 23. Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Intl. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE). LNCS. Springer, Heidelberg (2016)
[24] 24. Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varró, D. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol. 7793, pp. 146-162. Springer, Heidelberg (2013)
[25] 25. Beyer, D., Stahlbauer, A.: BDD-based software model checking with
[26] 26. Beyer, D., Wendler, P.: Reuse of verification results: conditional model checking, precision reuse, and verification witnesses. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol. 7976, pp. 1-17. Springer, Heidelberg (2013)
[27] 27. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1579, pp. 193-207. Springer, Heidelberg (1999)
[28] 28. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 196-207. ACM, New York (2003) · Zbl 1026.68514
[29] 29. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications. LNCS, vol. 735, pp. 128-141. Springer, Heidelberg (1993)
[30] 30. 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)
[31] 31. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677-691 (1986) · Zbl 0593.94022
[32] 32. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symp. on Principles of Programming Languages (POPL), pp. 289-300. ACM, New York (2009) · Zbl 1315.68085
[33] 33. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 57-70. ACM, New York (2010) · Zbl 1312.68056
[34] 34. 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) · Zbl 1325.68145
[35] 35. Clarke, E.M., Kröning, D., Sharygina, N., Yorav, K.:
[36] 36. Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M.G., Hermenegildo, M.: Improving abstract interpretations by combining domains. In: ACM Workshop on Partial Evaluation and Program Manipulation (PEPM), pp. 194-205. ACM, New York (1993)
[37] 37. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990) · Zbl 1158.68538
[38] 38. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Symp. on Principles of Programming Languages (POPL), pp. 238-252. ACM, New York (1977)
[39] 39. Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 269-282. ACM, New York (1979) · Zbl 1323.68356
[40] 40. Cousot, P., Cousot, R.: Formal language, grammar, and set-constraint-based program analysis by abstract interpretation. In: Intl. Conf. on Functional Programming Languages and Computer Architecture (FPCA), pp. 170-181. ACM, New York (1995)
[41] 41. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Symp. on Principles of Programming Languages (POPL), pp. 84-96. ACM, New York (1978)
[42] 42. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250-268 (1957) · Zbl 0081.24402
[43] 43. Damas, L., Milner, R.: Principal type schemes for functional languages. In: Symp. on Principles of Programming Languages (POPL), pp. 207-212. ACM, New York (1982)
[44] 44. Dams, D., Namjoshi, K.S.: Orion: high-precision methods for static error analysis of C and C++ programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Intl. Symp. on Formal Methods for Components and Objects (FMCO). LNCS, vol. 4111, pp. 138-160. Springer, Heidelberg (2005) · Zbl 1196.68039
[45] 45. Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., Fähndrich, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 7935, pp. 215-237. Springer, Heidelberg (2013)
[46] 46. Dudka, K., Peringer, P., Vojnar, T.: Predator: a shape analyzer based on symbolic memory graphs (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 412-414. Springer, Heidelberg (2014)
[47] 47. Ermis, E., Nutz, A., Dietsch, D., Hoenicke, J., Podelski, A.: Ultimate Kojak (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 421-423. Springer, Heidelberg (2014)
[48] 48. Falke, S., Merz, F., Sinz, C.L.: Improved bounded model checking of C programs using LLVM (competition contribution). 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. 623-626. Springer, Heidelberg (2013)
[49] 49. Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Intl. Symp. on Foundations of Software Engineering (FSE), pp. 227-236. ACM, New York (2005)
[50] 50. Geser, A., Knoop, J., Lüttgen, G., Rüthing, O., Steffen, B.: Non-monotone fixpoint iterations to resolve second-order effects. In: Gyimóthy, T. (ed.) Intl. Conf. on Compiler Construction (CC). LNCS, vol. 1060, pp. 106-120. Springer, Heidelberg (1996)
[51] 51. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNAI, vol. 4130, pp. 281-286. Springer, Heidelberg (2006)
[52] 52. Graf, S., Saïdi, H.: Construction of abstract state graphs with
[53] 53. Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: Hofmann, M., Felleisen, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 277-289. ACM, New York (2007) · Zbl 1295.68084
[54] 54. Gulwani, S., Juvekar, S.: Bound analysis using backward symbolic execution. Tech. Rep. MSR-TR-2009-156, Microsoft Research (2009)
[55] 55. Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Shao, Z., Pierce, B.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 239-251. ACM, New York (2009) · Zbl 1315.68094
[56] 56. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Necula, G.C., Wadler, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 235-246. ACM, New York (2008) · Zbl 1295.68085
[57] 57. Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 3148, pp. 212-227. Springer, Heidelberg (2004) · Zbl 1104.68414
[58] 58. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 281-292. ACM, New York (2008)
[59] 59. Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 5403, pp. 120-135. Springer, Heidelberg (2009) · Zbl 1206.68087
[60] 60. Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) European Symp. on Programming (ESOP). LNCS, vol. 3924, pp. 279-293. Springer, Heidelberg (2006) · Zbl 1178.68153
[61] 61. Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Schwartzbach, M.I., Ball, T. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 376-386. ACM, New York (2006)
[62] 62. Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 4349, pp. 363-377. Springer, Heidelberg (2007) · Zbl 1132.68470
[63] 63. Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5123, pp. 190-203. Springer, Heidelberg (2008) · Zbl 1155.68437
[64] 64. Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Zorn, B.G., Aiken, A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 292-304. ACM, New York (2010)
[65] 65. Gurfinkel, A., Albarghouthi, A., Chaki, S., Li, Y., Chechik, M.U.: Verification with interpolants and abstract interpretation (competition contribution). 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. 637-640. Springer, Heidelberg (2013)
[66] 66. Gurfinkel, A., Belov, A.: FrankenBit: bit-precise verification with many bits (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 408-411. Springer, Heidelberg (2014)
[67] 67. Heizmann, M., Christ, J., Dietsch, D., Hoenicke, J., Lindenmann, M., Musa, B., Schilling, C., Wissert, S., Podelski, A.: Ultimate Automizer with unsatisfiable cores (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 418-420. Springer, Heidelberg (2014)
[68] 68. Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Hung, D.V., Ogawa, M. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 8172, pp. 365-380. Springer, Heidelberg (2013) · Zbl 1410.68086
[69] 69. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 232-244. ACM, New York (2004) · Zbl 1325.68147
[70] 70. Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 526-538. Springer, Heidelberg (2002) · Zbl 1010.68507
[71] 71. 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
[72] 72. Inverso, O., Tomasco, E., Fischer, B., Torre, S.L., Parlato, G.: Lazy-CSeq: a lazy sequentialization tool for C (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 398-401. Springer, Heidelberg (2014)
[73] 73. Johannes, K., Helmut, V.:
[74] 74. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Intl. Conf. on Software Engineering (ICSE), pp. 215-224. ACM, New York (2010)
[75] 75. Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data-flow analysis and programs with recursive data structures. In: Symp. on Principles of Programming Languages (POPL), pp. 66-74. ACM, New York (1982)
[76] 76. Jung, Y., Kong, S., Wang, B.Y., Yi, K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: Barthe, G., Hermenegildo, M.V. (eds.) Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 5944, pp. 180-196. Springer, Heidelberg (2010) · Zbl 1248.68272
[77] 77. Kam, J., Ullman, J.: Global data-flow analysis and iterative algorithms. J. ACM 23(1), 158-171 (1976) · Zbl 0315.68031
[78] 78. Kennedy, K.: A survey of data-flow analysis techniques. In: Jones, N.D., Muchniek, S.S. (eds.) Program Flow Analysis: Theory and Applications, pp. 5-54. Prentice Hall, New York (1981)
[79] 79. Klein, M., Knoop, J., Koschützki, D., Steffen, B.: DFA&OPT-METAFrame: a tool kit for program analysis and optimization. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1055, pp. 422-426. Springer, Heidelberg (1996)
[80] 80. Knoop, J., Rüthing, O., Steffen, B.: Towards a tool kit for the automatic generation of interprocedural data-flow analyses. J. Program. Lang. 4(4), 211-246 (1996)
[81] 81. Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion. In: Conf. on Programming Language Design and Implementation (PLDI). ACM, New York (1992)
[82] 82. Knuth, D.E.: Semantics of context-free languages. Math. Syst. Theory 2(2), 127-145 (1968) · Zbl 0169.01401
[83] 83. Kong, S., Jung, Y., David, C., Wang, B.Y., Yi, K.: Automatically inferring quantified invariants via algorithmic learning from simple templates. In: Ueda, K. (ed.) Asian Symp. on Programming Languages and Systems (APLAS). LNCS, vol. 6461, pp. 328-343 (2010)
[84] 84. Kröning, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.: 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)
[85] 85. Kröning, D., Tautschnig, M.: CBMC: C bounded model checker (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 389-391. Springer, Heidelberg (2014)
[86] 86. Lewis, P., Rosenkrantz, D., Stearns, R.: Compiler Design Theory. Addison-Wesley, Reading (1976) · Zbl 0352.68004
[87] 87. Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 392-394. Springer, Heidelberg (2014)
[88] 88. Mohnen, M.: A graph-free approach to data-flow analysis. In: Horspool, R.N. (ed.) Intl. Conf. on Compiler Construction (CC). LNCS, vol. 2304, pp. 46-61. Springer, Heidelberg (2002) · Zbl 1051.68745
[89] 89. Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM 22(1) (1979) · Zbl 0393.68010
[90] 90. Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 405-407. Springer, Heidelberg (2014)
[91] 91. Muller, P., Vojnar, T.: CPAlien: shape analyzer for CPAchecker (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 395-397. Springer, Heidelberg (2014)
[92] 92. Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Jones, N.D., Leroy, X. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 330-341. ACM, New York (2004) · Zbl 1325.68068
[93] 93. Mycroft, A.: Polymorphic type schemes and recursive definitions. In: Paul, M., Robinet, B. (eds.) European Symp. on Programming (ESOP). LNCS, vol. 167, pp. 217-228. Springer, Heidelberg (1984) · Zbl 0548.68010
[94] 94. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999) · Zbl 0932.68013
[95] 95. Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory. Oxford University Press, Oxford (1990) · Zbl 0744.03029
[96] 96. Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 284-298. Springer, Heidelberg (2001) · Zbl 0978.68641
[97] 97. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002) · Zbl 0995.68018
[98] 98. 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
[99] 99. Popeea, C., Rybalchenko, A.: Threader: a verifier for multi-threaded programs (competition contribution). 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. 633-636. Springer, Heidelberg (2013)
[100] 100. Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural data-flow analysis via graph reachability. In: Cytron, R.K., Lee, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 49-61. ACM, New York (1995)
[101] 101. Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Symp. on Principles of Programming Languages (POPL), pp. 12-27. ACM, New York (1988)
[102] 102. Rothermel, G., Harrold, M.: Analyzing regression test selection techniques. IEEE Trans. Softw. Eng. 22(8), 529-551 (1996)
[103] 103. Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217-298 (2002)
[104] 104. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 3148, pp. 53-68. Springer, Heidelberg (2004) · Zbl 1104.68023
[105] 105. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Symp. on Principles of Programming Languages (POPL), pp. 318-329. ACM, New York (2004) · Zbl 1325.68071
[106] 106. Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn & Bacon, Needham Heights (1986)
[107] 107. Schmidt, D.A.: Data-flow analysis is model checking of abstract interpretations. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (1998)
[108] 108. Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 1503, pp. 351-380. Springer, Heidelberg (1998)
[109] 109. Shved, P., Mandrykin, M., Mutilin, V.: Predicate analysis with
[110] 110. Slaby, J., Strejcek, J.: Symbiotic 2: more precise slicing (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 415-417. Springer, Heidelberg (2014)
[111] 111. Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 223-234. ACM, New York (2009)
[112] 112. Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 313-326. ACM, New York (2010) · Zbl 1312.68068
[113] 113. Steffen, B.: Data-flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 536, pp. 346-365. Springer, Heidelberg (1991)
[114] 114. Steffen, B.: Generating data-flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115-139 (1993) · Zbl 0815.68070
[115] 115. Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 1145, pp. 22-41. Springer, Heidelberg (1996) · Zbl 1482.68095
[116] 116. Steffen, B., Claßen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 962, pp. 72-87. Springer, Heidelberg (1995)
[117] 117. Tomasco, E., Inverso, O., Fischer, B., Torre, S.L., Parlato, G.: MU-CSeq: sequentialization of C programs by shared memory unwindings (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 402-404. Springer, Heidelberg (2014)
[118] 118. Urban, C., Miné, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) European Symp. on Programming (ESOP). LNCS, vol. 8410, pp. 412-431. Springer, Heidelberg (2014) · Zbl 1405.68094
[119] 119. Vizel, Y., Grumberg, O., Shoham, S.: Intertwined forward-backward reachability analysis using interpolants. 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. 308-323. Springer, Heidelberg (2013) · Zbl 1381.68184
[120] 120. Šerý, O.: Enhanced property specification
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.