Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness

DOI10.1007/s10703-009-0073-1zbMath1185.68405OpenAlexW1994293250MaRDI QIDQ845242

Enea Zaffanella, Roberto Bagnara, Patricia M. Hill

Publication date: 5 February 2010

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-009-0073-1

zbMATH Keywords

UTVPI constraintsClosure by entailmentElimination of redundant constraintsKeywords: Abstract interpretationNumerical domainsWidening operators

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99)

Related Items

Compact Difference Bound Matrices, Sparsity preserving algorithms for octagons, On a generalization of Horn constraint systems, Integer feasibility and refutations in UTVPI constraints using bit-scaling, Analyzing fractional Horn constraint systems, PPLite: zero-overhead encoding of NNC polyhedra, Incremental closure for systems of two variables per inequality, The abstract domain of trapezoid step functions, Access-Based Localization for Octagons, Exact join detection for convex polyhedra and other numerical abstractions, A new look at the automatic synthesis of linear ranking functions, On integer closure in a system of unit two variable per inequality constraints, An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints, Transfer Function Synthesis without Quantifier Elimination, A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints, Incrementally closing octagons

Uses Software

• PPL
• Octagon
• ASTREE
• Zapato

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The octagon abstract domain
• Constraint propagation with interval labels
• Constructive versions of Tarski's fixed point theorems
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• Precise widening operators for convex polyhedra
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• Fast Decision Procedures Based on Congruence Closure
• Programming Languages and Systems
• Computer Aided Verification
• Programming Languages and Systems
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• Static Analysis
• Frontiers of Combining Systems
• The Transitive Reduction of a Directed Graph
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis