The two variable per inequality abstract domain

DOI10.1007/s10990-010-9062-8zbMath1232.68030OpenAlexW1991031013MaRDI QIDQ656848

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

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)

Related Items (6)

Injective convex polyhedra ⋮ Sparsity preserving algorithms for octagons ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ The two variable per inequality abstract domain ⋮ Transfer Function Synthesis without Quantifier Elimination ⋮ Incrementally closing octagons

Uses Software

• PPL
• PolyLib
• ASTREE

Cites Work

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

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