Abstract
Polyhedra abstract domain is one of the most expressive and used abstract domains for the static analysis of programs. Together with Kleene algorithm, it computes precise yet costly program invariants. Widening operators speed up this computation and guarantee its termination, but they often induce a loss of precision, especially for numerical programs. In this article, we present a process to accelerate Kleene iteration with a good trade-off between precision and computation time. For that, we use two tools: convex analysis to express the convergence of convex sets using support functions, and numerical analysis to accelerate this convergence applying sequence transformations. We demonstrate the efficiency of our method on benchmarks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amato, G., Parton, M., Scozzari, F.: Discovering invariants via simple component analysis. J. Symb. Comput. 47(12), 1533–1560 (2012)
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1-2), 28–56 (2005), http://dx.doi.org/10.1016/j.scico.2005.02.003
Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Formal Asp. Comput. 17(2), 222–257 (2005)
Bouissou, O., Seladji, Y.: Numerical abstract domain using support function. Presented at the Fifth International Workshop on Numerical Software Verification, http://www.lix.polytechnique.fr/~bouissou/pdf/bouissou_seladji_nsv_12.pdf
Bouissou, O., Seladji, Y., Chapoutot, A.: Acceleration of the abstract fixpoint computation in numerical program analysis. J. Symb. Comput. 47(12), 1479–1511 (2012)
Brezinski, C., Redivo Zaglia, M.: Extrapolation Methods-Theory and Practice. North-Holland (1991)
Brezinski, C., Redivo Zaglia, M.: Generalizations of Aitken’s process for accelerating the convergence of sequences. Comp. and Applied Math. 26(2) (2007)
Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Invited Paper. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84–97. ACM Press (1978)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM Press (1977)
Cox, A., Sankaranarayanan, S., Chang, B.-Y.E.: A Bit Too Precise? Bounded Verification of Quantized Digital Filters. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 33–47. Springer, Heidelberg (2012)
Delahaye, J.P., Germain-Bonne, B.: Résultats négatifs en accélération de la convergence. Numerische Mathematik 35, 443–457 (1980)
Feret, J.: Static Analysis of Digital Filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
Gonnord, L., Halbwachs, N.: Combining Widening and Acceleration in Linear Relation Analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006)
Gopan, D., Reps, T.W.: Guided Static Analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349–365. Springer, Heidelberg (2007)
Hiriart-Urrut, J.B., Lemaréchal, C.: Fundamentals of Convex Analysis. Springer (2004)
Jeannet, B., Miné, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)
Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with Thresholds for Programs with Complex Control Graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 492–502. Springer, Heidelberg (2011)
Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems (2010)
Löhne, A., Zălinescu, C.: On convergence of closed convex sets. Journal of Mathematical Analysis and Applications 319(2), 617–634 (2006)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Rockafellar, R.: Convex analysis, vol. 28. Princeton Univ. Pr. (1997)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable Analysis of Linear Systems Using Mathematical Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Sonntag, Y., Zălinescu, C.: Scalar convergence of convex sets. J. Math. Anal. Appl. 164(1), 219–241 (1992)
Wynn, P.: The epsilon algorithm and operational formulas of numerical analysis. Mathematics of Computation 15(74), 151–158 (1961)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seladji, Y., Bouissou, O. (2013). Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, vol 7737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35873-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-35873-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35872-2
Online ISBN: 978-3-642-35873-9
eBook Packages: Computer ScienceComputer Science (R0)