Simon, Axel and King, Andy and Howe, Jacob M. (2002) Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, Michael, ed. Logic Based Program Synthesis and Transformation 12th International Workshop. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 71-89. ISBN 978-3-540-40438-5. E-ISBN 978-3-540-45013-9. (doi:10.1007/3-540-45013-0_7) (KAR id:13681)
PDF
Language: English |
|
Download this file (PDF/391kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.1007/3-540-45013-0_7 |
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.
Item Type: | Book section |
---|---|
DOI/Identification number: | 10.1007/3-540-45013-0_7 |
Additional information: | see http://www.springer.de./comp/lncs/index.html |
Uncontrolled keywords: | Convex Hull, Logic Program, Linear Inequality, Abstract Interpretation, Abstract Domain |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Andy King |
Date Deposited: | 24 Nov 2008 17:59 UTC |
Last Modified: | 05 Nov 2024 09:47 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/13681 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):