×

zbMATH — the first resource for mathematics

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
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Amato, G.; Parton, M.; Scozzari, F., Deriving numerical abstract domains via principal component analysis, (), 134-150 · Zbl 1306.68018
[2] Amato, G.; Parton, M.; Scozzari, F., A tool which mines partial execution traces to improve static analysis, (), 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, (), 196-207
[6] Bourdoncle, F., Efficient chaotic iteration strategies with widenings, (), 128-141
[7] Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D. L.; Engler, D. R., Exe: automatically generating inputs of death, (), 322-335
[8] Chang, B.-Y.E.; Rival, X., Relational inductive shape analysis, (), 247-260 · Zbl 1295.68081
[9] Colóon, M.A.; Sipma, H.B., Synthesis of linear ranking functions, (), 67-81 · Zbl 0978.68095
[10] Cousot, P., The calculational design of a generic abstract interpreter, (), 421-506 · Zbl 0945.68032
[11] Cousot, P.; Cousot, R., Static determination of dynamic properties of programs, (), 106-130 · Zbl 0788.68094
[12] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (), 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, (), 84-97
[15] Dor, N.; Rodeh, M.; Sagiv, M., Cleanness checking of string manipulations in C programs via integer analysis, (), 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, (), 33-48 · Zbl 1126.68347
[18] Feret, J., The arithmetic-geometric progression abstract domain, (), 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. · Zbl 1342.68082
[20] Godefroid, P.; Klarlund, N.; Sen, K., Dart: directed automated random testing, (), 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, (), 370-384 · Zbl 1155.68366
[23] Gulwani, S.; Necula, G. C., Discovering affine equalities using random interpretation, (), 74-84 · Zbl 1321.68490
[24] Gulwani, S.; Necula, G. C., Precise interprocedural analysis using random interpretation, (), 324-337 · Zbl 1369.68139
[25] Guo, P.J.; Perkins, J.H.; McCamant, S.; Ernst, M.D., Dynamic inference of abstract types, (), 255-265
[26] Gupta, A.; Majumdar, R.; Rybalchenko, A., From tests to proofs, (), 262-276
[27] Gupta, A., Rybalchenko, A., 2009. InvGen: an efficient invariant generator. In: Bouajjani and Maler. pp. 634-640.
[28] Hausman, R.E., Constrained multivariate analysis, (), 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. Last accessed: 2010-06-11.
[31] 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)
[34] Miné, A., A new numerical abstract domain based on difference-bound matrices, (), 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. · Zbl 1126.68353
[36] 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, (), 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.
[40] O’Callahan, R. W.; Jackson, D., Lackwit: a program understanding tool based on type inference, (), 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.
[43] 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., (), 366-383
[46] Sankaranarayanan, S.; Sipma, H.B.; Manna, Z., Scalable analysis of linear systems using mathematical programming, (), 25-41 · Zbl 1111.68514
[47] Simon, A.; King, A.; Howe, J. M., Two variables per linear inequality as an abstract domain, (), 71-89 · Zbl 1278.68072
[48] Stursberg, O.; Krogh, B.H., Efficient representation and computation of reachable sets for hybrid systems, (), 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.
[50] Tillmann, N.; de Halleux, J., Pexwhite box test generation for.net, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.