Integer Polyhedra for Program Analysis: 5th International Conference, AAIM 2009, San Francisco, CA, USA, June 15-17, 2009. Proceedings

Part of book or chapter of book, Article English OPEN
Charles, Philip ; King, Andy ; Howe, Jacob M. (2009)

Polyhedra are widely used in model checking and abstract interpretation. Polyhedral analysis is effective when the relationships between variables are linear, but suffers from imprecision when it is necessary to take into account the integrality of the represented space. Imprecision also arises when non-linear constraints occur. Moreover, in terms of tractability, even a space defined by linear constraints can become unmanageable owing to the excessive number of inequalities. Thus it is useful to identify those inequalities whose omission has least impact on the represented space. This paper shows how these issues can be addressed in a novel way by growing the integer hull of the space and approximating the number of integral points within a bounded polyhedron.
  • References (2)

    1. S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition Systems. In Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 118-121. Springer-Verlag, 2003.

    2. A. Barvinok. Computing the Volume, Computing Integral Points, and Exponential Sums. In Computational Geometry, pages 161-170. ACM Press, 1992.

  • Metrics
    No metrics available
Share - Bookmark