×

Donut domains: efficient non-convex domains for abstract interpretation. (English) Zbl 1326.68094

Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 235-250 (2012).
Summary: Program analysis using abstract interpretation has been successfully applied in practice to find runtime bugs or prove software correct. Most abstract domains that are used widely rely on convexity for their scalability. However, the ability to express non-convex properties is sometimes required in order to achieve a precise analysis of some numerical properties. This work combines already known abstract domains in a novel way in order to design new abstract domains that tackle some non-convex invariants. The abstract objects of interest are encoded as a pair of two convex abstract objects: the first abstract object defines an over-approximation of the possible reached values, as is done customarily. The second abstract object under-approximates the set of impossible values within the state-space of the first abstract object. Therefore, the geometrical concretization of our objects is defined by a convex set minus another convex set (or hole). We thus call these domains donut domains.
For the entire collection see [Zbl 1236.68007].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Octagon; BOXES; GLPK; Apron
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Adjé, A., Gaubert, S., Goubault, E.: Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010) · Zbl 1260.68082 · doi:10.1007/978-3-642-11957-6_3
[2] Allamigeon, X., Gaubert, S., Goubault, É.: Inferring Min and Max Invariants Using Max-Plus Polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 189–204. Springer, Heidelberg (2008) · Zbl 1149.68346 · doi:10.1007/978-3-540-69166-2_13
[3] Bagnara, R.: A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. In: Science of Computer Programming, pp. 2–119 (1999) · Zbl 0891.68056
[4] Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Form. Asp. Comput., 222–257 (2005) · Zbl 1101.68674 · doi:10.1007/s00165-005-0061-1
[5] Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT 8(4-5), 449–466 (2006) · Zbl 05075103 · doi:10.1007/s10009-005-0215-8
[6] Bagnara, R., Hill, P.M., Zaffanella, E.: Exact join detection for convex polyhedra and other numerical abstractions. Comput. Geom. 43(5), 453–473 (2010) · Zbl 1187.65018 · doi:10.1016/j.comgeo.2009.09.002
[7] Bemporad, A., Filippi, C., Torrisi, F.D.: Inner and outer approximations of polytopes using boxes. Comput. Geom. 27(2), 151–178 (2004) · Zbl 1044.65016 · doi:10.1016/S0925-7721(03)00048-8
[8] Bemporad, A., Fukuda, K., Torrisi, F.D.: Convexity recognition of the union of polyhedra. Comput. Geom. 18(3), 141–154 (2001) · Zbl 0976.68163 · doi:10.1016/S0925-7721(01)00004-9
[9] Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: FMCAD, pp. 53–60. IEEE (2009) · doi:10.1109/FMCAD.2009.5351143
[10] Chen, L., Miné, A., Wang, J., Cousot, P.: Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 309–325. Springer, Heidelberg (2009) · Zbl 1248.68140 · doi:10.1007/978-3-642-03237-0_21
[11] Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Intl. Symp. on Programming, Dunod, France, pp. 106–130 (1976) · Zbl 0393.68080
[12] 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 (1977) · doi:10.1145/512950.512973
[13] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: POPL, pp. 84–97. ACM (January 1978) · doi:10.1145/512760.512770
[14] Dams, D., Namjoshi, K.S.: Automata as Abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 216–232. Springer, Heidelberg (2005) · Zbl 1112.68088 · doi:10.1007/978-3-540-30579-8_15
[15] Ghorbal, K., Goubault, E., Putot, S.: The Zonotope Abstract Domain Taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009) · Zbl 05571928 · doi:10.1007/978-3-642-02658-4_47
[16] Ghorbal, K., Goubault, E., Putot, S.: A Logical Product Approach to Zonotope Intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212–226. Springer, Heidelberg (2010) · Zbl 05772635 · doi:10.1007/978-3-642-14295-6_22
[17] Goldsztejn, A., Daney, D., Rueher, M., Taillibert, P.: Modal intervals revisited: a mean-value extension to generalized intervals. In: QCP (2005)
[18] Goubault, É., Putot, S.: Static Analysis of Numerical Algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006) · Zbl 1225.68073 · doi:10.1007/11823230_3
[19] Goubault, É., Putot, S.: Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 137–152. Springer, Heidelberg (2007) · Zbl 1211.68088 · doi:10.1007/978-3-540-74061-2_9
[20] Granger, P.: Static Analysis of Linear Congruence Equalities Among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991) · Zbl 0967.68509 · doi:10.1007/3-540-53982-4_10
[21] Gurfinkel, A., Chaki, S.: Boxes: A Symbolic Abstract Domain of Boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287–303. Springer, Heidelberg (2010) · Zbl 1306.68026 · doi:10.1007/978-3-642-15769-1_18
[22] Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of Linear Hybrid Systems by Means of Convex Approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994) · doi:10.1007/3-540-58485-4_43
[23] 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) · Zbl 05571933 · doi:10.1007/978-3-642-02658-4_52
[24] Kanade, A., Alur, R., Ivančić, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 430–445. Springer, Heidelberg (2009) · Zbl 05571914 · doi:10.1007/978-3-642-02658-4_33
[25] Makhorin, A.: The GNU Linear Programming Kit, GLPK (2000), http://www.gnu.org/software/glpk/glpk.html
[26] Masdupuy, F.: Array abstractions using semantic analysis of trapezoid congruences. In: ICS, pp. 226–235 (1992) · doi:10.1145/143369.143414
[27] Miné, A.: The octagon abstract domain. In: WCRE, pp. 310–319 (October 2001) · doi:10.1109/WCRE.2001.957836
[28] Prabhu, P., Maeda, N., Balakrishnan, G., Ivančić, F., Gupta, A.: Interprocedural Exception Analysis for C++. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 583–608. Springer, Heidelberg (2011) · Zbl 05942533 · doi:10.1007/978-3-642-22655-7_27
[29] Péron, M., Halbwachs, N.: An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 268–282. Springer, Heidelberg (2007) · Zbl 1132.68464 · doi:10.1007/978-3-540-69738-1_20
[30] Rockafellar, R.T.: Convex Analysis. Princeton University Press (1970) · Zbl 0193.18401 · doi:10.1515/9781400873173
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.