The two variable per inequality abstract domain

DOI10.1007/S10990-010-9062-8zbMATH Open1232.68030OpenAlexW1991031013MaRDI QIDQ656848FDOQ656848

Authors: Axel Simon, Andy King 

Publication date: 13 January 2012

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://kar.kent.ac.uk/30678/1/tvpi-rev.pdf

Recommendations

• Two variables per linear inequality as an abstract domain
• Incremental closure for systems of two variables per inequality
• The octagon abstract domain
• Generalizing the template polyhedral domain
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships

zbMATH Keywords

integer programmingabstract interpretationpolyhedral analysis

Mathematics Subject Classification ID

Integer programming (90C10) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• The octagon abstract domain
• Introduction to algorithms
• Title not available (Why is that?)
• An efficient algorithm for determining the convex hull of a finite planar set
• Title not available (Why is that?)
• A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
• Constructive versions of Tarski's fixed point theorems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Another efficient algorithm for convex hulls in two dimensions
• Program Analysis Using Symbolic Ranges
• Abstract interpretation and application to logic programs
• Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality
• Title not available (Why is that?)
• Algorithm for discovering the set of all the solutions of a linear programming problem
• A fast convex hull algorithm
• Title not available (Why is that?)
• Deciding Linear Inequalities by Computing Loop Residues
• On the Average Number of Maxima in a Set of Vectors and Applications
• The two variable per inequality abstract domain
• Convex hull of planarh-polyhedra
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• Convex hulls of finite sets of points in two and three dimensions
• Two variables per linear inequality as an abstract domain
• Title not available (Why is that?)
• Widening Polyhedra with Landmarks
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Static Analysis
• A polynomial combinatorial algorithm for generalized minimum cost flow
• Monotonizing linear programs with up to two nonzeroes per column
• Computing Two-Dimensional Integer Hulls
• A reevaluation of an efficient algorithm for determining the convex hull of a finite planar set
• A more efficient convex hull algorithm
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• A class of polynomially solvable range constraints for interval analysis without widenings
• Analyzing string buffers in C
• Title not available (Why is that?)
• Splitting the Control Flow with Boolean Flags
• A counterexample to an algorithm for computing monotone hulls of simple polygons
• On the SUP-INF Method for Proving Presburger Formulas
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concurrency theory. Calculi and automata for modelling untimed and timed cocurrent systems.
• Title not available (Why is that?)
• Static Analysis
• Some ways to reduce the space dimension in polyhedra computations

Cited In (10)

• Abstract interpretation of microcontroller code: intervals meet congruences
• Incremental closure for systems of two variables per inequality
• Incrementally closing octagons
• Sparsity preserving algorithms for octagons
• An abstract domain to discover interval linear equalities
• Injective convex polyhedra
• Two variables per linear inequality as an abstract domain
• The two variable per inequality abstract domain
• Transfer function synthesis without quantifier elimination
• Logahedra: a new weakly relational domain

Uses Software

• PPL
• PolyLib
• ASTREE

This page was built for publication: The two variable per inequality abstract domain

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q656848)