The two variable per inequality abstract domain

DOI10.1007/S10990-010-9062-8MaRDI QIDQ656848zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

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

Describes a project that uses

Uses Software

• ASTREE
• PolyLib
• PPL

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)