Abstract
The abstract domain of polyhedra lies at the heart of many program analysis techniques. However, its operations can be expensive, precluding their application to polyhedra that involve many variables. This paper describes a new approach to computing polyhedral domain operations. The core of this approach is an algorithm to calculate variable elimination (projection) based on parametric linear programming. The algorithm enumerates only non-redundant inequalities of the projection space, hence permits anytime approximation of the output.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Amenta, N., Ziegler, G.: Shadows and Slices of Polytopes. In: Symposium on Computational Geometry, pp. 10–19. ACM Press (1996)
Avis, D.: lrs: A Revised Implementation of the Reverse Search Vertex Enumeration Algorithm. In: Kalai, G., Ziegler, G.M. (eds.) Polytopes – Combinatorics and Computation, pp. 177–198. Brikhäuser, Basel (2000)
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming 72(1-2), 3–21 (2008)
Boyd, S., Vandenberghe, S.: Convex Optimization. Cambridge University Press (2004)
Burger, E.: Über Homogene Lineare Ungleichungssysteme. Zeitschrift für Angewandte Mathematik und Mechanik 36, 135–139 (1956)
Chernikova, N.V.: Algorithm for Discovering the Set of All the Solutions of a Linear Programming Problem. Computational Mathematics and Mathematical Physics 8(6), 1387–1395 (1968)
Chvátal, V.: Linear Programming. W.H. Freeman and Company (1983)
Clarisó, R., Cortadella, J.: The Octahedron Abstract Domain. Science of Computer Programming 64(1), 115–139 (2007)
Colón, M.A., Sankaranarayanan, S.: Generalizing the Template Polyhedral Domain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 176–195. Springer, Heidelberg (2011)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: Principles of Programming Languages, pp. 84–97. ACM Press (1978)
Dantzig, G.B., Orchard-Hays, W.: The Product Form for the Inverse in the Simplex Method. Mathematical Tables and other Aids to Computation 8(46), 64–67 (1954)
Duffin, R.J.: On Fourier’s Analysis of Linear Inequality Systems. Mathematical Programming Studies 1, 71–95 (1974)
Flexeder, A., Müller-Olm, M., Petter, M., Seidl, H.: Fast Interprocedural Linear Two-Variable Equalities. ACM Transactions on Programming Languages and Systems 33(6) (2011)
Fulara, J., Durnoga, K., Jakubczyk, K., Shubert, A.: Relational Abstract Domain of Weighted Hexagons. Electronic Notes in Theoretical Computer Science 267(1), 59–72 (2010)
Gass, S., Saaty, T.: The Computational Algorithm for the Parametric Objective Function. Naval Research Logistics Quarterly 2(1-2), 39–45 (1955)
Howe, J.M., King, A.: Logahedra: A New Weakly Relational Domain. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306–320. Springer, Heidelberg (2009)
Imbert, J.-L.: Fourier’s Elimination: Which to Choose?. In: First Workshop on Principles and Practice of Constraint Programming, pp. 117–129 (1993)
Jarvis, R.A.: On the identification of the convex hull of a finite set of points in the plane. Information Processing Letters 2(1), 18–21 (1973)
Jones, C.N., Kerrigan, E.C., Maciejowski, J.M.: On Polyhedral Projection and Parametric Programming. Journal of Optimization Theory and Applications 138(2), 207–220 (2008)
Jones, C.N., Maciejowski, J.M.: Reverse Search for Parametric Linear Programming. In: IEEE Conference on Decision and Control, pp. 1504–1509 (2006)
Khachiyan, L., Boros, E., Borys, K., Elbassioni, K., Gurvich, V.: Generating All Vertices of a Polyhedron is Hard. Discrete and Computational Geometry 39, 174–190 (2008)
Kohler, D.A.: Projections of Convex Polyhedral Sets. Technical Report 67-29, Operations Research Centre, University of California, Berkeley (1967)
Lassez, J.-L., Huynh, T., McAloon, K.: Simplification and Elimination of Redundant Linear Arithmetic Constraints. In: Benhamou, F., Colmerauer, A. (eds.) Constraint Logic Programming, pp. 73–87. MIT Press (1993)
Le Verge, H.: A Note on Chernikova’s algorithm. Technical Report 1662, Institut de Recherche en Informatique, Campus Universitaire de Beaulieu, France (1992)
Miné, A.: A New Numerical Abstract Domain Based on Difference-Bound Matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Miné, A.: The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Motzkin, T.S.: Beiträge zur Theorie der Linearen Ungleichungen. PhD thesis, Universität Zurich (1936)
Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The Double Description Method. In: Annals of Mathematics Studies, vol. 2, pp. 51–73. Princeton University Press (1953)
Ponce, J., Sullivan, S., Sudsang, A., Boissonnat, J.-D., Merlet, J.-P.: On Computing Four-Finger Equilibrium and Force-Closure Grasps of Polyhedral Objects. International Journal of Robotics Research 16(2), 11–35 (1997)
Sankaranarayanan, S., Colón, M.A., Sipma, H., Manna, Z.: Efficient Strongly Relational Polyhedral Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111–125. Springer, Heidelberg (2005)
Seidl, H., Flexeder, A., Petter, M.: Interprocedurally Analysing Linear Inequality Relations. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 284–299. Springer, Heidelberg (2007)
Simon, A., King, A.: Exploiting Sparsity in Polyhedral Analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005)
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)
Todd, M.J.: The Many Facets of Linear Programming. Mathematical Programming 91(3), 417–436 (2002)
Wilde, D.K.: A Library for Doing Polyhedral Operations. Technical Report 785, Institut de Recherche en Informatique, Campus Universitaire de Beaulieu, France (1993)
Ziegler, G.M.: Lectures on Polytopes. Springer (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Howe, J.M., King, A. (2012). Polyhedral Analysis Using Parametric Objectives. In: Miné, A., Schmidt, D. (eds) Static Analysis. SAS 2012. Lecture Notes in Computer Science, vol 7460. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33125-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-33125-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33124-4
Online ISBN: 978-3-642-33125-1
eBook Packages: Computer ScienceComputer Science (R0)