Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
type: Item
instance of: scholarly article
title: Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
zbMATH Open document ID: 1185.68405
author: Roberto Bagnara
author: Patricia M. Hill
author: Enea Zaffanella
published in: Formal Methods in System Design
publication date: 2010-02-05T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M99
zbMATH DE Number: 5666997
zbMATH Keywords: Keywords: Abstract interpretation
zbMATH Keywords: Numerical domains
zbMATH Keywords: Widening operators
zbMATH Keywords: Closure by entailment
zbMATH Keywords: Elimination of redundant constraints
zbMATH Keywords: UTVPI constraints
describes a project that uses: PPL
describes a project that uses: ASTREE
describes a project that uses: Zapato
describes a project that uses: Octagon
MaRDI profile type: Publication
full work available at URL: s10703-009-0073-1
OpenAlex ID: W1994293250
cites work: Q4174789
cites work: A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
cites work: Q4529777
cites work: Static Analysis
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Q4411954
cites work: The Computational Complexity of Simultaneous Diophantine Approximation Problems
cites work: Computer Aided Verification
cites work: Programming Languages and Systems
cites work: An Improved Tight Closure Algorithm for Integer Octagonal Constraints
cites work: Q5532570
cites work: Constructive versions of Tarski's fixed point theorems
cites work: Q3241581
cites work: Constraint propagation with interval labels
cites work: Precise widening operators for convex polyhedra
cites work: The Transitive Reduction of a Directed Graph
cites work: Q4414726
cites work: Q4424848
cites work: Frontiers of Combining Systems
cites work: The octagon abstract domain
cites work: Fast Decision Procedures Based on Congruence Closure
DOI: 10.1007/S10703-009-0073-1
Recommended article: Towards Abstraction-Based Verification of Shape Calculus
Recommended article: Static Analysis
Recommended article: Q4411954
Recommended article: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
Recommended article: Q4414398
Recommended article: Relational Mathematics for Relative Correctness
Recommended article: Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
Recommended article: Efficient Symbolic Representations for Arithmetic Constraints in Verification
Recommended article: Tools and Algorithms for the Construction and Analysis of Systems
Recommended article: Lifting numeric relational domains to algebraic data types
description: scientific article; zbMATH DE number 5666997