Acceleration of the abstract fixpoint computation in numerical program analysis. (English) Zbl 1244.68029
Summary: Static analysis by abstract interpretation aims at automatically proving properties of computer programs, by computing invariants that over-approximate the program behaviors. These invariants are defined as the least fixpoint of a system of semantic equations and are most often computed using the Kleene iteration. This computation may not terminate so specific solutions were proposed to deal with this issue. Most of the proposed methods sacrifice the precision of the solution to guarantee the termination of the computation in a finite number of iterations.
In this article, we define a new method which allows to obtain a precise fixpoint in a short time. The main idea is to use numerical methods designed for accelerating the convergence of numerical sequences. These methods were primarily designed to transform a convergent, real valued sequence into another sequence that converges faster to the same limit.
We show how they can be integrated into the Kleene iteration in order to improve the fixpoint computation in the abstract interpretation framework. An interesting feature of our method is that it remains very close to the Kleene iteration and thus can be easily implemented in existing static analyzers. We describe a general framework and its application to two numerical abstract domains: the interval domain and the octagon domain. Experimental results show that the number of iterations and the time needed to compute the fixpoint undergo a significant reduction compared to the Kleene iteration, while its precision is preserved.
In this article, we define a new method which allows to obtain a precise fixpoint in a short time. The main idea is to use numerical methods designed for accelerating the convergence of numerical sequences. These methods were primarily designed to transform a convergent, real valued sequence into another sequence that converges faster to the same limit.
We show how they can be integrated into the Kleene iteration in order to improve the fixpoint computation in the abstract interpretation framework. An interesting feature of our method is that it remains very close to the Kleene iteration and thus can be easily implemented in existing static analyzers. We describe a general framework and its application to two numerical abstract domains: the interval domain and the octagon domain. Experimental results show that the number of iterations and the time needed to compute the fixpoint undergo a significant reduction compared to the Kleene iteration, while its precision is preserved.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 65B99 | Acceleration of convergence in numerical analysis |
Keywords:
abstract numerical domains; acceleration of convergence; numerical sequence transformation; widening operator with thresholds; Kleene iteration; fixpointReferences:
| [1] | Bardin, S.; Finkel, A.; Leroux, J.; Petrucci, L., FAST: acceleration from theory to practice, Journal on Software Tools for Technology Transfer, 10, 5, 401-424 (2008) |
| [2] | Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, (The Essence of Computation: Complexity, Analysis, Transformation. The Essence of Computation: Complexity, Analysis, Transformation, LNCS, vol. 2566 (2002), Springer), 85-108 · Zbl 1026.68514 |
| [3] | Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., A static analyzer for large safety-critical software, (Programming Language Design and Implementation (2003), ACM Press), 196-207 |
| [4] | Bouissou, O.; Seladji, Y.; Chapoutot, A., Abstract fixpoint computations with numerical acceleration methods, Electronic Notes in Theoretical Computer Science, 267, 1, 29-42 (2010), Proceeding of the Second International Workshop on Numerical and Symbolic Abstract Domains: NSAD 2010 · Zbl 1342.68071 |
| [5] | Bourdoncle, F., Efficient chaotic iteration strategies with widenings, (International Conference on Formal Methods in Programming and their Applications (1993), Springer-Verlag), 128-141 |
| [6] | Brezinski, C.; Redivo Zaglia, M., Extrapolation Methods-Theory and Practice (1991), North-Holland · Zbl 0744.65004 |
| [7] | Brezinski, C.; Redivo Zaglia, M., Generalizations of Aitken’s process for accelerating the convergence of sequences, Computational and Applied Mathematics (2007) · Zbl 1182.65007 |
| [8] | Brezinski, C.; Redivo Zaglia, M., A review of vector convergence acceleration methods, with applications to linear algebra problems, International Journal of Quantum Chemistry, 109, 8, 1631-1639 (2008) |
| [9] | Costan, A.; Gaubert, S.; Goubault, E.; Martel, M.; Putot, S., A policy iteration algorithm for computing fixed points in static analysis of programs, (Computer Aided Verification. Computer Aided Verification, LNCS, vol. 3576 (2005), Springer), 462-475 · Zbl 1081.68616 |
| [10] | Cousot, P., Semantic foundations of program, (Program Flow Analysis: Theory and Applications (1981), Prentice-Hall), 303-342, (Chapter 10) |
| [11] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Symposium on Principles of Programming Languages (1977), ACM Press), 238-252 |
| [12] | Cousot, P.; Cousot, R., Abstract interpretation frameworks, Journal of Logic and Computation, 2, 4, 511-547 (1992) · Zbl 0783.68073 |
| [13] | Cousot, P.; Cousot, R., Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, (Programming Language Implementation and Logic Programming. Programming Language Implementation and Logic Programming, LNCS, vol. 631 (1992), Springer), 269-295 |
| [14] | Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (Symposium on Principles of Programming Languages (1978), ACM Press), 84-97 |
| [15] | Feret, J., Static analysis of digital filter, (European Symposium on Programming. European Symposium on Programming, LNCS, No. 2986 (2004), Springer) · Zbl 1126.68347 |
| [16] | Gaubert, S.; Goubault, E.; Taly, A.; Zennou, S., Static analysis by policy iteration on relational domains, (European Symposium on Programming. European Symposium on Programming, LNCS, vol. 4421 (2007), Springer), 237-252 · Zbl 1187.68151 |
| [17] | Gonnord, L.; Halbwachs, N., Combining widening and acceleration in linear relation analysis, (Static Analysis Symposium. Static Analysis Symposium, LNCS, vol. 4134 (2006), Springer), 144-160 · Zbl 1225.68071 |
| [18] | Gopan, D.; Reps, T. W., Lookahead widening, (Computer Aided Verification. Computer Aided Verification, LNCS, vol. 4144 (2006), Springer), 452-466 |
| [19] | Gopan, D.; Reps, T. W., Guided static analysis, (Static Analysis Symposium. Static Analysis Symposium, LNCS, vol. 4634 (2007), Springer), 349-365 · Zbl 1211.68087 |
| [20] | Goubault, E.; Martel, M.; Putot, S., Asserting the precision of floating-point computations: a simple abstract interpreter, (European Symposium on Programming. European Symposium on Programming, LNCS, vol. 2305 (2002), Springer), 209-212 · Zbl 1077.68615 |
| [21] | Goubault, E.; Putot, S., Static analysis of numerical algorithms, (Symposium on Static Analysis. Symposium on Static Analysis, LNCS, vol. 4134 (2006), Springer), 18-34 · Zbl 1225.68073 |
| [22] | Goubault, E.; Putot, S., Static analysis of finite precision computations, (Jhala, R.; Schmidt, D. A., VMCAI. VMCAI, Lecture Notes in Computer Science, vol. 6538 (2011), Springer), 232-247 · Zbl 1317.68116 |
| [23] | Goubault, E.; Putot, S.; Baufreton, P.; Gassino, J., Static analysis of the accuracy in control systems: principles and experiments, (Formal methods for industrial critical systems. Formal methods for industrial critical systems, LNCS, vol. 4916 (2007), Springer-Verlag), 3-20 |
| [24] | Graves-Morris, P. R., Extrapolation methods for vector sequences, Numerische Mathematik, 61, 4, 475-487 (1992) · Zbl 0765.65004 |
| [25] | Halbwachs, N.; Proy, Y.-E.; Roumanoff, P., Verification of real-time systems using linear relation analysis, Formal Methods in System Design, 11, 2, 157-185 (1997) |
| [26] | Jeannet, B.; Miné, A., APRON: A library of numerical abstract domains for static analysis, (Computer Aided Verification. Computer Aided Verification, LNCS, vol. 5643 (2009)), 661-667 |
| [27] | Le Verge, H., 1992. A note on Chernikova’s Algorithm. Tech. Rep. 635, IRISA, Rennes, France.; Le Verge, H., 1992. A note on Chernikova’s Algorithm. Tech. Rep. 635, IRISA, Rennes, France. |
| [28] | Leroux, J.; Sutre, G., Accelerated data-flow analysis, (Static Analysis Symposium. Static Analysis Symposium, LNCS, vol. 4634 (2007), Springer), 184-199 · Zbl 1211.68093 |
| [29] | Miné, A., Relational abstract domains for the detection of floating-point run-time errors, (European Symposium on Programming. European Symposium on Programming, LNCS, vol. 2986 (2004), Springer), 3-17 · Zbl 1126.68353 |
| [30] | Miné, A., The octagon abstract domain, Higher-Order and Symbolic Computation, 19, 1, 31-100 (2006) · Zbl 1105.68069 |
| [31] | Monniaux, D., Compositional analysis of floating-point linear numerical filters, (Computer-Aided Verification. Computer-Aided Verification, Lecture Notes in Computer Science, No. 3576 (2005), Springer Verlag), 199-212 · Zbl 1081.93028 |
| [32] | Müller-Olm, M.; Seidl, H., Computing polynomial program invariants, Information Processing Letters, 91, 5, 233-244 (2004) · Zbl 1177.68048 |
| [33] | Rodriguez-Carbonell, E.; Kapur, D., Generating all polynomial invariants in simple loops, Journal of Symbolic Computation, 42, 4, 443-476 (2007) · Zbl 1121.13034 |
| [34] | Rudin, W., Principles of Mathematical Analysis (1976), McGraw-Hill · Zbl 0148.02903 |
| [35] | Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Scalable analysis of linear systems using mathematical programming, (Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 3385 (2005), Springer), 25-41 · Zbl 1111.68514 |
| [36] | Schrammel, P.; Jeannet, B., Extending abstract acceleration methods to data-flow programs with numerical inputs, Electronic Notes in Theoretical Computer Science, 267, 1, 101-114 (2010), Proceeding of the Second International Workshop on Numerical and Symbolic Abstract Domains: NSAD 2010 · Zbl 1342.68100 |
| [37] | Simon, A.; King, A., Widening polyhedra with landmarks, (Asian Symposium on Programming Languages and Systems. Asian Symposium on Programming Languages and Systems, LNCS, vol. 4279 (2006), Springer), 166-182 · Zbl 1168.68365 |
| [38] | Simon, A.; King, A.; Howe, J., Two variables per linear inequality as an abstract domain, (Logic Based Program Synthesis and Transformation. Logic Based Program Synthesis and Transformation, LNCS, vol. 2664 (2003)), 955-974 |
| [39] | Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5, 285-309 (1955) · Zbl 0064.26004 |
| [40] | Winskel, G., The Formal Semantics of Programming Languages (1993), MIT Press · Zbl 0919.68082 |
| [41] | Wynn, P., The epsilon algorithm and operational formulas of numerical analysis, Mathematics of Computation, 15, 74, 151-158 (1961) · Zbl 0102.33205 |
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.
