Abstract
Linear relation analysis (polyhedral analysis), devoted to discovering linear invariant relations among variables of a program, remains one of the most powerful abstract interpretations but is subject to convexity limitations. Absolute value enjoys piecewise linear expressiveness and thus natively fits to encode certain non-convex properties. Based on this insight, we propose to use linear absolute value relation analysis to discover linear relations among values and absolute values of program variables. Under the framework of abstract interpretation, the analysis yields a new numerical abstract domain, namely the abstract domain of linear absolute value inequalities (Σ k a k x k + Σ k b k |x k | ≤ c), which can be used to analyze programs involving piecewise linear behaviors (e.g., due to conditional branches or absolute value function calls). Experimental results of our prototype are encouraging; The new abstract domain can find non-convex invariants of interest in practice.
This work is supported by the INRIA project “Abstraction” common to CNRS and ENS in France, and by the National Natural Science Foundation of China under Grant No.60725206.
Chapter PDF
Similar content being viewed by others
Keywords
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
Gnu multiple precision arithmetic library, http://gmplib.org/ .
Allamigeon, X., Gaubert, S., Goubault, E.: 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)
Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135–148. Springer, Heidelberg (2004)
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)
Chua, L.O., Deng, A.-C.: Canonical piecewise-linear representation. IEEE Trans. on Circuits and Systems 35(1), 101–111 (1988)
Cottle, R.W., Pang, J.-S., Stone, R.E.: The Linear Complementarity Problem. Academic Press, New York (1992)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM POPL 1979, pp. 269–282. ACM Press, New York (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978, pp. 84–96. ACM Press, New York (1978)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co, New York (1979)
Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program 32(1-3), 177–210 (1998)
Granger, P.: Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 165–199 (1989)
Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 370–384. Springer, Heidelberg (2008)
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)
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)
Lalire, G., Argoud, M., Jeannet, B.: Interproc., http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/
Laviron, V., Logozzo, F.: Subpolyhedra: A (more) scalable approach to infer linear inequalities. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229–244. Springer, Heidelberg (2009)
LeVerge, H.: A note on Chernikova’s algorithm. Technical Report 635, IRISA, France (1992)
Mangasarian, O.L., Pang, J.S.: The extended linear complementarity problem. SIAM J. Matrix Anal. Appl. 16(2), 359–368 (1995)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems (TOPLAS) 29(5) (2007)
Rohn, J.: Solvability of systems of interval linear equations and inequalities. In: Linear Optimization Problems with Inexact Data, pp. 35–77. Springer, Heidelberg (2006)
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)
Sankaranarayanan, S., Sipma, H., 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)
Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., Chichester (1986)
Simon, A.: Splitting the Control Flow with Boolean Flags. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 315–331. Springer, Heidelberg (2008)
Simon, A., King, A., Howe, J.M.: Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, L., Miné, A., Wang, J., Cousot, P. (2011). Linear Absolute Value Relation Analysis. In: Barthe, G. (eds) Programming Languages and Systems. ESOP 2011. Lecture Notes in Computer Science, vol 6602. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19718-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-19718-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19717-8
Online ISBN: 978-3-642-19718-5
eBook Packages: Computer ScienceComputer Science (R0)