Skip to main content
SpringerLink
Log in

Two Variables per Linear Inequality as an Abstract Domain

  • Conference paper
  • First Online:
Logic Based Program Synthesis and Transformation (LOPSTR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2664))

Abstract

This paper explores the spatial domain of sets of inequalities where each inequality contains at most two variables — a domain that is richer than intervals and more tractable than general polyhedra. We present a complete suite of efficient domain operations for linear systems with two variables per inequality with unrestricted coefficients. We exploit a tactic in which a system of inequalities with at most two variables per inequality is decomposed into a series of projections — one for each two dimensional plane. The decomposition enables all domain operations required for abstract interpretation to be expressed in terms of the two dimensional case. The resulting operations are efficient and include a novel planar convex hull algorithm. Empirical evidence suggests that widening can be applied effectively, ensuring tractability.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Bagnara. Data-Flow Analysis for Constrant Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, 1997.

    Google Scholar 

  2. V. Balasundaram and K. Kennedy. A Technique for Summarizing Data Access and its Use in Parallelism Enhancing Transformations. In Programming Language Design and Implementation, pages 41–53. ACM Press, 1989.

    Google Scholar 

  3. F. Bancilhon and R. Ramakrishnan. An Amateur’s Introduction to Recursive Query Processing Strategies. In International Conference on Management of Data, pages 16–52. ACM Press, 1986.

    Google Scholar 

  4. F. Benoy and A. King. Inferring Argument Size Relationships with CLP(ℝ). In Logic Program Synthesis and Transformation (Selected Papers), volume 1207 of Lecture Notes in Computer Science, pages 204–223. Springer-Verlag, 1997.

    Google Scholar 

  5. J. L. Bentley, H. T. Kung, M. Schkolnick, and C. D. Thompson. On the Average Number of Maxima in a Set of Vectors. Journal of the ACM, 25:536–543, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  6. N. V. Chernikova. Algorithm for Discovering the Set of All Solutions of a Linear Programming Problem. USSR Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.

    Article  MATH  Google Scholar 

  7. P. Cousot and R. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295. Springer-Verlag, 1992.

    Chapter  Google Scholar 

  8. P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In Principles of Programming Languages, pages 84–97. ACM Press, 1978.

    Google Scholar 

  9. E. Davis. Constraint Propagation with Interval Labels. Artificial Intelligence, 32(3):281–331, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  10. S. D. Feit. A Fast Algorithm for the Two-Variable Integer Programming Problem. Journal of the ACM, 31(1):99–113, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  11. R. L. Graham. An Efficient Algorithm for Determining the Convex Hull of a Finite Planar Set. Information Processing Letters, 1(4):132–133, 1972.

    Article  MATH  Google Scholar 

  12. P. Granger. Static Analysis of Linear Congruence Equalities among Variables of a Program. In International Joint Conference on the Theory and Practice of Software Development, volume 493 of Lecture Notes in Computer Science, pages 169–192. Springer-Verlag, 1991.

    Google Scholar 

  13. W. H. Harrison. Compiler Analysis of the Value Ranges for Variables. IEEE Transactions on Software Engineering, SE-3(3), 1977.

    Google Scholar 

  14. W. Harvey. Computing Two-Dimensional Integer Hulls. SIAM Journal on Computing, 28(6):2285–2299, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  15. W. Harvey and P. J. Stuckey. A Unit Two Variable per Inequality Integer Constraint Solver for Constraint Logic Programming. Australian Computer Science Communications, 19(1):102–111, 1997.

    Google Scholar 

  16. D. S. Hochbaum and J. Naor. Simple and Fast Algorithms for Linear and Integer Programs with Two Variables per Inequality. SIAM Journal on Computing, 23(6):1179–1192, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  17. J. M. Howe and A. King. Specialising Finite Domain Programs using Polyhedra. In Logic Programming, Synthesis and Transformation (Selected Papers), volume 1817 of Lecture Notes in Computer Science, pages 118–135. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  18. J. Jaffar, M. J. Maher, P. J. Stuckey, and R. H. C. Yap. Beyond Finite Domains. In International Workshop on Principles and Practice of Constraint Programming, volume 874 of Lecture Notes in Computer Science, pages 86–94. Springer-Verlag, 1994.

    Google Scholar 

  19. M. Karr. Affine Relationships Among Variables of a Program. Acta Informatica, 6:133–151, 1976.

    Article  MATH  MathSciNet  Google Scholar 

  20. V. Klee and G. J. Minty. How Good is the Simplex Algorithm? In Inequalities-III. Academic Press, New York and London, 1972.

    Google Scholar 

  21. J. C. Lagarias. The Computational Complexity of Simultaneous Diophantine Approximation Problems. SIAM Journal on Computing, 14(1):196–209, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  22. K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Clock Difference Diagrams. Nordic Journal of Computing, 6(3):271–298, 1999.

    MATH  MathSciNet  Google Scholar 

  23. H. Le Verge. A Note on Chernikova’s Algorithm. Technical Report 1662, Institut de Recherche en Informatique, Campus Universitaire de Beaulieu, France, 1992.

    Google Scholar 

  24. N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs. In International Conference on Logic Programming, pages 63–77. MIT Press, 1997.

    Google Scholar 

  25. A. Miné. A New Numerical Abstract Domain Based on Difference-Bound Matrices. In Programs as Data Objects, volume 2053 of Lecture Notes in Computer Science, pages 155–172. Springer, 2001.

    Chapter  Google Scholar 

  26. A. Miné. The Octagon Abstract Domain. In Eighth Working Conference on Reverse Engineering, pages 310–319. IEEE Computer Society, 2001.

    Google Scholar 

  27. A. Miné. A Few Graph-Based Relational Numerical Abstract Domains. In Ninth International Static Analysis Symposium, volume 2477 of Lecture Notes in Computer Science, pages 117–132. Springer-Verlag, 2002.

    Google Scholar 

  28. J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference Decision Diagrams. In Conference of the European Association for Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111–125. Springer-Verlag, 1999.

    Google Scholar 

  29. C. G. Nelson. An n log(n) Algorithm for the Two-Variable-Per-Constraint Linear Programming Satisfiability Problem. Technical Report STAN-CS-78-689, Stanford University, Department of Computer Science, 1978.

    Google Scholar 

  30. V. R. Pratt. Two Easy Theories Whose Combination is Hard, September 1977. http://boole.stanford.edu/pub/sefnp.pdf.

  31. H. Raynaud. Sur L’enveloppe Convexe des Nuages de Points Aléatoires dans ℝn. Journal of Applied Probability, 7(1):35–48, 1970.

    Article  MATH  MathSciNet  Google Scholar 

  32. R. Seidel. Convex Hull Computations. In J. E. Goodman and J. O’Rourke, editors, Handbook of Discrete and Computational Geometry, pages 361–376. CRC Press, 1997.

    Google Scholar 

  33. R. Shaham, H. Kolodner, and M. Sagiv. Automatic Removal of Array Memory Leaks in Java. In Compiler Construction, volume 1781 of Lecture Notes in Computer Science, pages 50–66. Springer, 2000.

    Chapter  Google Scholar 

  34. R. Shostak. Deciding Linear Inequalities by Computing Loop Residues. Journal of the ACM, 28(4): 769–779, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  35. Z. Su and D. Wagner. Efficient Algorithms for General Classes of Integer Range Constraints, July 2001. http://www.cs.berkeley.edu/~zhendong/.

  36. D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A First Step Towards Detection of Buffer Overrun Vulnerabilities. In Network and Distributed System Security Symposium. Internet Society, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Kent, Canterbury, UK

    Axel Simon & Andy King

  2. Department of Computing, City University, London, UK

    Jacob M. Howe

Authors
  1. Axel Simon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jacob M. Howe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Leuschel

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Simon, A., King, A., Howe, J.M. (2003). Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2002. Lecture Notes in Computer Science, vol 2664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45013-0_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-45013-0_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40438-5

  • Online ISBN: 978-3-540-45013-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation