Abstract
We introduce a new numerical abstract domain able to infer min and max invariants over the program variables, based on max-plus polyhedra. Our abstraction is more precise than octagons, and allows to express non-convex properties without any disjunctive representations. We have defined sound abstract operators, evaluated their complexity, and implemented them in a static analyzer. It is able to automatically compute precise properties on numerical and memory manipulating programs such as algorithms on strings and arrays.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Abstract Interpretation
- Minimal System
- Abstract Domain
- Disjunctive Representation
- Numerical Abstract Domain
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, Springer, Heidelberg (2001)
Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2001)
Dor, N., Rodeh, M., Sagiv, M.: Cssv: towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI 2003, ACM Press, New York (2003)
Allamigeon, X., Godard, W., Hymans, C.: Static Analysis of String Manipulations in Critical Embedded C Programs. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM TOPLAS 29(5) (2007)
Karr, M.: Affine relationships among variables of a program. Acta Inf. 6 (1976)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, Tucson, Arizona, USA. ACM Press, New York (1978)
Zimmermann, K.: A general separation theorem in extremal algebras. Ekonom.-Mat. Obzor. 13(2), 179–201 (1977)
Litvinov, G., Maslov, V., Shpiz, G.: Idempotent functional analysis: an algebraical approach. Math. Notes 69(5), 696–729 (2001); Also eprint arXiv:math.FA/0009128
Gaubert, S., Plus, M.: Methods and applications of (max,+) linear algebra. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, Springer, Heidelberg (1997)
Cohen, G., Gaubert, S., Quadrat, J.P.: Max-plus algebra and system theory: where we are and where to go now. Annual Reviews in Control 23, 207–219 (1999)
Develin, M., Sturmfels, B.: Tropical convexity. Doc. Math. 9, 1–27 (2004)
Cohen, G., Gaubert, S., Quadrat, J.P.: Duality and separation theorem in idempotent semimodules. Linear Algebra and Appl. 379, 395–422 (2004)
Joswig, M.: Tropical halfspaces. In: Combinatorial and computational geometry. Math. Sci. Res. Inst. Publ., vol. 52. Cambridge Univ. Press, Cambridge (2005)
Cohen, G., Gaubert, S., Quadrat, J.P., Singer, I.: Max-plus convex sets and functions. In: Litvinov, G.L., Maslov, V.P. (eds.) Idempotent Mathematics and Mathematical Physics. Contemporary Mathematics, vol. 377, pp. 105–129. AMS (2005)
Gaubert, S., Katz, R.: Max-plus convex geometry. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 192–206. Springer, Heidelberg (2006)
Butkovič, P., Schneider, H., Sergeev, S.: Generators, extremals and bases of max cones. Linear Algebra Appl. 421, 394–406 (2007)
Gaubert, S., Katz, R.: The Minkowski theorem for max-plus convex sets. Linear Algebra and Appl. 421, 356–369 (2006)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, Los Angeles, California. ACM Press, New York (1977)
Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3–17. Springer, Heidelberg (2006)
Giacobazzi, R., Ranzato, F.: Compositional Optimization of Disjunctive Abstract Interpretations. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol. 1058, Springer, Heidelberg (1996)
Sotin, P., Cachera, D., Jensen, T.: Quantitative static analysis over semirings: analysing cache behaviour for java card. In: QAPL 2006. ENTCS, vol. 1380, Elsevier, Amsterdam (2006)
Butkovič, P., Hegedüs, G.: An elimination method for finding all solutions of the system of linear equations over an extremal algebra. Ekonomicko-matematicky Obzor. 20(2), 203–215 (1984)
Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics 8(6), 282–293 (1968)
Le Verge, H.: A note on Chernikova’s algorithm (1992)
Gaubert, S., Katz, R.: External and internal representation of max-plus polyhedra. Privately circuled draft (2008)
Baccelli, F., Cohen, G., Olsder, G.J., Quadrat, J.P.: Synchronization and Linearity. Wiley, Chichester (1992)
Cohen, G., Gaubert, S., Quadrat, J.P.: Regular matrices in max-plus algebra (preprint, 2008)
Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3eme cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (March 1979)
Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2) (August 1997)
Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005)
Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. SIGPLAN Not. 40(1) (2005)
Allamigeon, X.: Non-disjunctive Numerical Domain for Array Predicate Abstraction. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 163–177. Springer, Heidelberg (2008)
Batcher, K.: Sorting networks and their applications. In: Proceedings of the AFIPS Spring Joint Computer Conference 32, pp. 307–314 (1968)
Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905. Springer, Heidelberg (2008)
Gaubert, S., Gunawardena, J.: The duality theorem for min-max functions. C. R. Acad. Sci. Paris. 326 (Série I), 43–48 (1998)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Allamigeon, X., Gaubert, S., Goubault, É. (2008). Inferring Min and Max Invariants Using Max-Plus Polyhedra. In: Alpuente, M., Vidal, G. (eds) Static Analysis. SAS 2008. Lecture Notes in Computer Science, vol 5079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69166-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-69166-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69163-1
Online ISBN: 978-3-540-69166-2
eBook Packages: Computer ScienceComputer Science (R0)