×

Discovering invariants via simple component analysis. (English) Zbl 1246.65077

Summary: We propose a new technique combining dynamic and static analysis of programs to find linear invariants. We use a statistical tool, called simple component analysis, to analyze partial execution traces of a given program. We get a new coordinate system in the vector space of program variables, which is used to specialize numerical abstract domains. As an application, we instantiate our technique to interval analysis of simple imperative programs and show some experimental evaluations.

MSC:

65G40 General methods in interval analysis
65C60 Computational problems in statistics (MSC2010)
62H25 Factor analysis and principal components; correspondence analysis
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amato, G.; Parton, M.; Scozzari, F., Deriving numerical abstract domains via principal component analysis, (Cousot, R.; Martel, M., 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings. 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings, Lecture Notes in Computer Science. Springer, vol. 6337 (2010), Berlin Heidelberg), 134-150 · Zbl 1306.68018
[2] Amato, G.; Parton, M.; Scozzari, F., A tool which mines partial execution traces to improve static analysis, (Barringer, H.; etal., First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings. First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings, Lecture Notes in Computer Science., vol. 6418 (2010), Springer: Springer Berlin Heidelberg), 475-479
[3] Anaya-Izquierdo, K.; Critchley, F.; Vines, K., Orthogonal simple component analysis: a new, exploratory approach, Annals of Applied Statistics, 5, 1, 486-522 (March 2011)
[4] Bagnara, R.; Hill, P. M.; Zaffanella, E., The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Science of Computer Programming, 72, 1-2, 3-21 (2008)
[5] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., A static analyzer for large safety-critical software, (Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI’03 (June 7-14 2003), ACM Press: ACM Press San Diego, California, USA), 196-207
[6] Bourdoncle, F., Efficient chaotic iteration strategies with widenings, (Bjørner, D.; Broy, M.; Pottosin, I. V., Formal Methods in Programming and Their Applications, International Conference Academgorodok, Novosibirsk, Russia June 28-July 2, 1993 Proceedings. Formal Methods in Programming and Their Applications, International Conference Academgorodok, Novosibirsk, Russia June 28-July 2, 1993 Proceedings, Lecture Notes in Computer Science, vol. 735 (1993), Springer: Springer Berlin Heidelberg), 128-141
[7] Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D. L.; Engler, D. R., Exe: automatically generating inputs of death, (Proceedings of the 13th ACM Conference on Computer and Communications Security. Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS’06 (2006), ACM: ACM New York, NY, USA), 322-335
[8] Chang, B.-Y. E.; Rival, X., Relational inductive shape analysis, (Principles Of Programming Languages. Principles Of Programming Languages, POPL’08. Principles Of Programming Languages. Principles Of Programming Languages, POPL’08, SIGPLAN Not., vol. 43(1) (2008), ACM: ACM New York, NY, USA), 247-260 · Zbl 1295.68081
[9] Colóon, M. A.; Sipma, H. B., Synthesis of linear ranking functions, (Margaria, T.; Yi, W., Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings, Lecture Notes in Computer Science, vol. 2031 (2001), Springer: Springer Berlin Heidelberg), 67-81 · Zbl 0978.68095
[10] Cousot, P., The calculational design of a generic abstract interpreter, (Broy, M.; Steinbrüggen, R., Calculational System Design. NATO Science Series F (1999), IOS Press: IOS Press Amsterdam), 421-506 · Zbl 0945.68032
[11] Cousot, P.; Cousot, R., Static determination of dynamic properties of programs, (Proceedings of the Second International Symposium on Programming (1976), Dunod: Dunod Paris, France), 106-130 · Zbl 0788.68094
[12] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (POPL’79: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Jan. 1979), ACM Press: ACM Press New York, NY, USA), 269-282 · Zbl 0788.68094
[13] Cousot, P.; Cousot, R., Abstract interpretation and applications to logic programs, The Journal of Logic Programming, 13, 2-3, 103-179 (Jul. 1992)
[14] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (POPL’78: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Jan. 1978), ACM Press: ACM Press New York, NY, USA), 84-97
[15] Dor, N.; Rodeh, M.; Sagiv, M., Cleanness checking of string manipulations in C programs via integer analysis, (Cousot, P., Static Analysis, 8th International Symposium, SAS 2001 Paris, France, July 16-18, 2001 Proceedings. Static Analysis, 8th International Symposium, SAS 2001 Paris, France, July 16-18, 2001 Proceedings, Lecture Notes in Computer Science, vol. 2126 (2001), Springer: Springer Berlin Heidelberg), 194-212 · Zbl 0997.68570
[16] Ernst, M. D.; Cockrell, J.; Griswold, W. G.; Notkin, D., Dynamically discovering likely program invariants to support program evolution, IEEE Transactions on Software Engineering, 27, 2, 99-123 (2001)
[17] Feret, J., Static analysis of digital filters, (Schmidt (2004)), 33-48 · Zbl 1126.68347
[18] Feret, J., The arithmetic-geometric progression abstract domain, (Cousot, R., Verification, Model Checking, and Abstract Interpretation-6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings. Verification, Model Checking, and Abstract Interpretation-6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings, Lecture Notes in Computer Science, vol. 3385 (2005), Springer), 42-58 · Zbl 1111.68504
[19] Fulara, J., Durnoga, K., Jakubczyk, K., Schubert, A., October 2010. Relational abstract domain of weighted hexagons. Electronic Notes in Theoretical Computer Science 267, 59-72. http://dx.doi.org/10.1016/j.entcs.2010.09.006; Fulara, J., Durnoga, K., Jakubczyk, K., Schubert, A., October 2010. Relational abstract domain of weighted hexagons. Electronic Notes in Theoretical Computer Science 267, 59-72. http://dx.doi.org/10.1016/j.entcs.2010.09.006 · Zbl 1342.68082
[20] Godefroid, P.; Klarlund, N.; Sen, K., Dart: directed automated random testing, (Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’05 (2005), ACM: ACM New York, NY, USA), 213-223
[21] Granger, P., Static analysis of arithmetical congruences, International Journal of Computer Mathematics, 32 (1989) · Zbl 0679.68022
[22] Gulavani, B. S.; Gulwani, S., A numerical abstract domain based on expression abstraction and max operator with application in timing analysis, (Gupta, A.; Malik, S., Computer Aided Verification, 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings. Computer Aided Verification, 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings, Lecture Notes in Computer Science, vol. 5123 (2008), Springer: Springer Berlin Heidelberg), 370-384 · Zbl 1155.68366
[23] Gulwani, S.; Necula, G. C., Discovering affine equalities using random interpretation, (Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL’03 (2003), ACM: ACM New York, NY, USA), 74-84 · Zbl 1321.68490
[24] Gulwani, S.; Necula, G. C., Precise interprocedural analysis using random interpretation, (Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’05 (2005), ACM: ACM New York, NY, USA), 324-337 · Zbl 1369.68139
[25] Guo, P. J.; Perkins, J. H.; McCamant, S.; Ernst, M. D., Dynamic inference of abstract types, (Proceedings of the 2006 International Symposium on Software Testing and Analysis. Proceedings of the 2006 International Symposium on Software Testing and Analysis, ISSTA’06 (2006), ACM: ACM New York, NY, USA), 255-265
[26] Gupta, A.; Majumdar, R.; Rybalchenko, A., From tests to proofs, (Kowalewski, S.; Philippou, A., Tools and Algorithms for the Construction and Analysis of Systems 15th International Conference, TACAS 2009, York, UK, March 22-29, 2009. Proceedings. Tools and Algorithms for the Construction and Analysis of Systems 15th International Conference, TACAS 2009, York, UK, March 22-29, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5505 (2009), Springer: Springer Berlin Heidelberg), 262-276
[27] Gupta, A., Rybalchenko, A., 2009. InvGen: an efficient invariant generator. In: Bouajjani and Maler. pp. 634-640.; Gupta, A., Rybalchenko, A., 2009. InvGen: an efficient invariant generator. In: Bouajjani and Maler. pp. 634-640.
[28] Hausman, R. E., Constrained multivariate analysis, (Optimization in statistics. Optimization in statistics, Stud. Management Sci., vol. 19 (1982), North-Holland: North-Holland Amsterdam), 137-151
[29] Hickey, T. J.; Ju, Q.; van Emden, M. H., Interval arithmetic: from principles to implementation, Journal of the ACM, 48, 1038-1068 (2001) · Zbl 1323.65047
[30] Jeannet, B., 2004. Interproc Analyzer for Recursive Programs with Numerical Variables. INRIA, software and documentation are available at the following URL: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi; Jeannet, B., 2004. Interproc Analyzer for Recursive Programs with Numerical Variables. INRIA, software and documentation are available at the following URL: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
[31] Jeannet, B., Miné, A., 2009. APRON: a library of numerical abstract domains for static analysis. In: Bouajjani and Maler. pp. 661-667.; Jeannet, B., Miné, A., 2009. APRON: a library of numerical abstract domains for static analysis. In: Bouajjani and Maler. pp. 661-667.
[32] Karr, M., Affine relationships among variables of a program, Acta Information, 6, 133-151 (1976) · Zbl 0358.68025
[33] Kearfott, R. B., Interval computations: Introduction, uses, and resources, Euromath Bulletin, 2, 95-112 (1996) · Zbl 1465.65041
[34] Miné, A., A new numerical abstract domain based on difference-bound matrices, (Danvy, O.; Filinski, A., Programs as Data Objects, Second Symposium, PADO2001 Aarhus, Denmark, May 21-23, 2001 Proceeding. Programs as Data Objects, Second Symposium, PADO2001 Aarhus, Denmark, May 21-23, 2001 Proceeding, Lecture Notes in Computer Science, vol. 2053 (2001), Springer: Springer Berlin Heidelberg), 155-172 · Zbl 0984.68034
[35] Miné, A., 2004. Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt. pp. 3-17.; Miné, A., 2004. Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt. pp. 3-17. · Zbl 1126.68353
[36] Miné, A., 2004. Weakly relational numerical abstract domains. Ph.D. Thesis, École Polytechnique.; Miné, A., 2004. Weakly relational numerical abstract domains. Ph.D. Thesis, École Polytechnique.
[37] Miné, A., The octagon abstract domain, Higher-Order and Symbolic Computation, 19, 1, 31-100 (Mar. 2006)
[38] Miné, A., Symbolic methods to enhance the precision of numerical abstract domains, (Emerson, E. A.; Namjoshi, K. S., Verification, Model Checking, and Abstract Interpretation. 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006. Proceedings. Verification, Model Checking, and Abstract Interpretation. 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006. Proceedings, Lecture Notes in Computer Science, vol. 3855 (2006), Springer: Springer Berlin Heidelberg), 348-363 · Zbl 1176.68050
[39] O’Callahan, R.W., 2001. Generalized aliasing as a basis for program analysis tools. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, PA, USA, aAI3051029.; O’Callahan, R.W., 2001. Generalized aliasing as a basis for program analysis tools. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, PA, USA, aAI3051029.
[40] O’Callahan, R. W.; Jackson, D., Lackwit: a program understanding tool based on type inference, (Proceedings of the 19th International Conference on Software Engineering. Proceedings of the 19th International Conference on Software Engineering, ICSE’97 (1997), ACM: ACM New York, NY, USA), 338-348
[41] Pearson, K., On lines and planes of closest fit to systems of points in space, Philosophical Magazine, 2, 6, 559-572 (1901) · JFM 32.0710.04
[42] R Development Core Team 2009. R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing, Vienna, Austria. http://www.R-project.org; R Development Core Team 2009. R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing, Vienna, Austria. http://www.R-project.org
[43] Rohn, J., Apr. 2010. Inverse interval matrix: A survey. Tech. Rep. V-1073, Academy of Sciences of the Czech Republic.; Rohn, J., Apr. 2010. Inverse interval matrix: A survey. Tech. Rep. V-1073, Academy of Sciences of the Czech Republic. · Zbl 1223.15009
[44] Rousson, V.; Gasser, T., Simple component analysis, Journal of the Royal Statistical Society. Series C, 53, 4, 539-555 (2004) · Zbl 1111.62310
[45] Sankaranarayanan, S.; Ivančić, F.; Gupta, A., (Nielson, H. R.; Filé, G., Static Analysis, 14th International Symposium. Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007. Static Analysis, 14th International Symposium. Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Lecture Notes in Computer Science, vol. 4634 (2007), Springer: Springer Berlin Heidelberg), 366-383 · Zbl 1211.68101
[46] Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Scalable analysis of linear systems using mathematical programming, (Cousot, R., Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings. Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings, Lecture Notes in Computer Science, vol. 3385 (January 2005), Springer: Springer Berlin Heidelberg), 25-41 · Zbl 1111.68514
[47] Simon, A.; King, A.; Howe, J. M., Two variables per linear inequality as an abstract domain, (Leuschel, M., Logic Based Program Synthesis and Transformation 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20, 2002. Revised Selected Papers. Logic Based Program Synthesis and Transformation 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20, 2002. Revised Selected Papers, Lecture Notes in Computer Science, vol. 2664 (2003), Springer: Springer Berlin Heidelberg), 71-89 · Zbl 1278.68072
[48] Stursberg, O.; Krogh, B. H., Efficient representation and computation of reachable sets for hybrid systems, (Maler, O.; Pnueli, A., Hybrid Systems: Computation and Control. 6th InternationalWorkshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003. Proceedings. Hybrid Systems: Computation and Control. 6th InternationalWorkshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003. Proceedings, Lecture Notes in Computer Science, vol. 2623 (2003), Springer: Springer Berlin Heidelberg), 482-497 · Zbl 1032.93037
[49] The Open University, 1983. MDST242 Statistics in Society, Unit C3: Is my child normal? The Open University, figure 3.12.; The Open University, 1983. MDST242 Statistics in Society, Unit C3: Is my child normal? The Open University, figure 3.12.
[50] Tillmann, N.; de Halleux, J., Pexwhite box test generation for.net, (Beckert, B.; Hahnle, R., Tests and Proofs. Tests and Proofs, Lecture Notes in Computer Science, vol. 4966 (2008), Springer), 134-153
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.