An Improved Tight Closure Algorithm for Integer Octagonal Constraints

DOI10.1007/978-3-540-78163-9_6MaRDI QIDQ5452703zbMATH OpenOpenAlexFDO

Authors Roberto Bagnara, Patricia M. Hill, Enea Zaffanella

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78163-9_6

Mathematics Subject Classification ID

Programming involving graphs or networks (90C35) Graph theory (including graph drawing) in computer science (68R10) Nonnumerical algorithms (68W05)

Recommendations

• On integer closure in a system of unit two variable per inequality constraints
• An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints
• Incrementally closing octagons
• Simple and efficient algorithms for octagons
• Incremental satisfiability and implication for UTVPI constraints

Cites work

• scientific article; zbMATH DE number 1638645 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• Computer Aided Verification
• Fast Decision Procedures Based on Congruence Closure
• Frontiers of Combining Systems
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• Programming Languages and Systems
• Static Analysis
• Static analysis of arithmetical congruences
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• The octagon abstract domain

Cited in

(21)

• Incremental closure for systems of two variables per inequality
• Iterating Octagons
• Formalizing the face lattice of polyhedra
• Incrementally closing octagons
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• scientific article; zbMATH DE number 7215283 (Why is no real title available?)
• Ranking functions for linear-constraint loops
• Algorithms for tight spans and tropical linear spaces
• On integer closure in a system of unit two variable per inequality constraints
• Splitting the Control Flow with Boolean Flags
• Simple and efficient algorithms for octagons
• Certified abstract cost analysis
• An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints
• A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
• Exact join detection for convex polyhedra and other numerical abstractions
• Trichotomy for integer linear systems based on their sign patterns
• Pattern Matching and Parameter Identification for Parametric Timed Regular Expressions
• Solving non-linear Horn clauses using a linear Horn clause solver
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• A combinatorial certifying algorithm for linear feasibility in UTVPI constraints

Describes a project that uses

Uses Software

• PPL

This page was built for publication: An Improved Tight Closure Algorithm for Integer Octagonal Constraints

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